from sympy.assumptions.assume import global_assumptions from sympy.assumptions.cnf import CNF, EncodedCNF from sympy.assumptions.ask import Q from sympy.logic.inference import satisfiable from sympy.logic.algorithms.lra_theory import UnhandledInput, ALLOWED_PRED from sympy.matrices.kind import MatrixKind from sympy.core.kind import NumberKind from sympy.assumptions.assume import AppliedPredicate from sympy.core.mul import Mul from sympy.core.singleton import S def lra_satask(proposition, assumptions=True, context=global_assumptions): """ Function to evaluate the proposition with assumptions using SAT algorithm in conjunction with an Linear Real Arithmetic theory solver. Used to handle inequalities. Should eventually be depreciated and combined into satask, but infinity handling and other things need to be implemented before that can happen. """ props = CNF.from_prop(proposition) _props = CNF.from_prop(~proposition) cnf = CNF.from_prop(assumptions) assumptions = EncodedCNF() assumptions.from_cnf(cnf) context_cnf = CNF() if context: context_cnf = context_cnf.extend(context) assumptions.add_from_cnf(context_cnf) return check_satisfiability(props, _props, assumptions) # Some predicates such as Q.prime can't be handled by lra_satask. # For example, (x > 0) & (x < 1) & Q.prime(x) is unsat but lra_satask would think it was sat. # WHITE_LIST is a list of predicates that can always be handled. WHITE_LIST = ALLOWED_PRED | {Q.positive, Q.negative, Q.zero, Q.nonzero, Q.nonpositive, Q.nonnegative, Q.extended_positive, Q.extended_negative, Q.extended_nonpositive, Q.extended_negative, Q.extended_nonzero, Q.negative_infinite, Q.positive_infinite} def check_satisfiability(prop, _prop, factbase): sat_true = factbase.copy() sat_false = factbase.copy() sat_true.add_from_cnf(prop) sat_false.add_from_cnf(_prop) all_pred, all_exprs = get_all_pred_and_expr_from_enc_cnf(sat_true) for pred in all_pred: if pred.function not in WHITE_LIST and pred.function != Q.ne: raise UnhandledInput(f"LRASolver: {pred} is an unhandled predicate") for expr in all_exprs: if expr.kind == MatrixKind(NumberKind): raise UnhandledInput(f"LRASolver: {expr} is of MatrixKind") if expr == S.NaN: raise UnhandledInput("LRASolver: nan") # convert old assumptions into predicates and add them to sat_true and sat_false # also check for unhandled predicates for assm in extract_pred_from_old_assum(all_exprs): n = len(sat_true.encoding) if assm not in sat_true.encoding: sat_true.encoding[assm] = n+1 sat_true.data.append([sat_true.encoding[assm]]) n = len(sat_false.encoding) if assm not in sat_false.encoding: sat_false.encoding[assm] = n+1 sat_false.data.append([sat_false.encoding[assm]]) sat_true = _preprocess(sat_true) sat_false = _preprocess(sat_false) can_be_true = satisfiable(sat_true, use_lra_theory=True) is not False can_be_false = satisfiable(sat_false, use_lra_theory=True) is not False if can_be_true and can_be_false: return None if can_be_true and not can_be_false: return True if not can_be_true and can_be_false: return False if not can_be_true and not can_be_false: raise ValueError("Inconsistent assumptions") def _preprocess(enc_cnf): """ Returns an encoded cnf with only Q.eq, Q.gt, Q.lt, Q.ge, and Q.le predicate. Converts every unequality into a disjunction of strict inequalities. For example, x != 3 would become x < 3 OR x > 3. Also converts all negated Q.ne predicates into equalities. """ # loops through each literal in each clause # to construct a new, preprocessed encodedCNF enc_cnf = enc_cnf.copy() cur_enc = 1 rev_encoding = {value: key for key, value in enc_cnf.encoding.items()} new_encoding = {} new_data = [] for clause in enc_cnf.data: new_clause = [] for lit in clause: if lit == 0: new_clause.append(lit) new_encoding[lit] = False continue prop = rev_encoding[abs(lit)] negated = lit < 0 sign = (lit > 0) - (lit < 0) prop = _pred_to_binrel(prop) if not isinstance(prop, AppliedPredicate): if prop not in new_encoding: new_encoding[prop] = cur_enc cur_enc += 1 lit = new_encoding[prop] new_clause.append(sign*lit) continue if negated and prop.function == Q.eq: negated = False prop = Q.ne(*prop.arguments) if prop.function == Q.ne: arg1, arg2 = prop.arguments if negated: new_prop = Q.eq(arg1, arg2) if new_prop not in new_encoding: new_encoding[new_prop] = cur_enc cur_enc += 1 new_enc = new_encoding[new_prop] new_clause.append(new_enc) continue else: new_props = (Q.gt(arg1, arg2), Q.lt(arg1, arg2)) for new_prop in new_props: if new_prop not in new_encoding: new_encoding[new_prop] = cur_enc cur_enc += 1 new_enc = new_encoding[new_prop] new_clause.append(new_enc) continue if prop.function == Q.eq and negated: assert False if prop not in new_encoding: new_encoding[prop] = cur_enc cur_enc += 1 new_clause.append(new_encoding[prop]*sign) new_data.append(new_clause) assert len(new_encoding) >= cur_enc - 1 enc_cnf = EncodedCNF(new_data, new_encoding) return enc_cnf def _pred_to_binrel(pred): if not isinstance(pred, AppliedPredicate): return pred if pred.function in pred_to_pos_neg_zero: f = pred_to_pos_neg_zero[pred.function] if f is False: return False pred = f(pred.arguments[0]) if pred.function == Q.positive: pred = Q.gt(pred.arguments[0], 0) elif pred.function == Q.negative: pred = Q.lt(pred.arguments[0], 0) elif pred.function == Q.zero: pred = Q.eq(pred.arguments[0], 0) elif pred.function == Q.nonpositive: pred = Q.le(pred.arguments[0], 0) elif pred.function == Q.nonnegative: pred = Q.ge(pred.arguments[0], 0) elif pred.function == Q.nonzero: pred = Q.ne(pred.arguments[0], 0) return pred pred_to_pos_neg_zero = { Q.extended_positive: Q.positive, Q.extended_negative: Q.negative, Q.extended_nonpositive: Q.nonpositive, Q.extended_negative: Q.negative, Q.extended_nonzero: Q.nonzero, Q.negative_infinite: False, Q.positive_infinite: False } def get_all_pred_and_expr_from_enc_cnf(enc_cnf): all_exprs = set() all_pred = set() for pred in enc_cnf.encoding.keys(): if isinstance(pred, AppliedPredicate): all_pred.add(pred) all_exprs.update(pred.arguments) return all_pred, all_exprs def extract_pred_from_old_assum(all_exprs): """ Returns a list of relevant new assumption predicate based on any old assumptions. Raises an UnhandledInput exception if any of the assumptions are unhandled. Ignored predicate: - commutative - complex - algebraic - transcendental - extended_real - real - all matrix predicate - rational - irrational Example ======= >>> from sympy.assumptions.lra_satask import extract_pred_from_old_assum >>> from sympy import symbols >>> x, y = symbols("x y", positive=True) >>> extract_pred_from_old_assum([x, y, 2]) [Q.positive(x), Q.positive(y)] """ ret = [] for expr in all_exprs: if not hasattr(expr, "free_symbols"): continue if len(expr.free_symbols) == 0: continue if expr.is_real is not True: raise UnhandledInput(f"LRASolver: {expr} must be real") # test for I times imaginary variable; such expressions are considered real if isinstance(expr, Mul) and any(arg.is_real is not True for arg in expr.args): raise UnhandledInput(f"LRASolver: {expr} must be real") if expr.is_integer == True and expr.is_zero != True: raise UnhandledInput(f"LRASolver: {expr} is an integer") if expr.is_integer == False: raise UnhandledInput(f"LRASolver: {expr} can't be an integer") if expr.is_rational == False: raise UnhandledInput(f"LRASolver: {expr} is irational") if expr.is_zero: ret.append(Q.zero(expr)) elif expr.is_positive: ret.append(Q.positive(expr)) elif expr.is_negative: ret.append(Q.negative(expr)) elif expr.is_nonzero: ret.append(Q.nonzero(expr)) elif expr.is_nonpositive: ret.append(Q.nonpositive(expr)) elif expr.is_nonnegative: ret.append(Q.nonnegative(expr)) return ret