Public Member Functions | |
def | __init__ (self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None) |
def | __deepcopy__ (self, memo={}) |
def | __del__ (self) |
def | depth (self) |
def | inconsistent (self) |
def | prec (self) |
def | precision (self) |
def | size (self) |
def | __len__ (self) |
def | get (self, i) |
def | __getitem__ (self, arg) |
def | assert_exprs (self, *args) |
def | append (self, *args) |
def | insert (self, *args) |
def | add (self, *args) |
def | convert_model (self, model) |
def | __repr__ (self) |
def | sexpr (self) |
def | dimacs (self) |
def | translate (self, target) |
def | __copy__ (self) |
def | __deepcopy__ (self, memo={}) |
def | simplify (self, *arguments, **keywords) |
def | as_expr (self) |
![]() | |
def | use_pp (self) |
Data Fields | |
ctx | |
goal | |
Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible). Goals are processed using Tactics. A Tactic transforms a goal into a set of subgoals. A goal has a solution if one of its subgoals has a solution. A goal is unsatisfiable if all subgoals are unsatisfiable.
def __init__ | ( | self, | |
models = True , |
|||
unsat_cores = False , |
|||
proofs = False , |
|||
ctx = None , |
|||
goal = None |
|||
) |
Definition at line 5160 of file z3py.py.
def __del__ | ( | self | ) |
def __copy__ | ( | self | ) |
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
def __getitem__ | ( | self, | |
arg | |||
) |
def __len__ | ( | self | ) |
Return the number of constraints in the goal `self`. >>> g = Goal() >>> len(g) 0 >>> x, y = Ints('x y') >>> g.add(x == 0, y > x) >>> len(g) 2
Definition at line 5254 of file z3py.py.
Referenced by AstVector.__getitem__(), and AstVector.__setitem__().
def __repr__ | ( | self | ) |
def add | ( | self, | |
* | args | ||
) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.add(x > 0, x < 2) >>> g [x > 0, x < 2]
Definition at line 5332 of file z3py.py.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
def append | ( | self, | |
* | args | ||
) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.append(x > 0, x < 2) >>> g [x > 0, x < 2]
def as_expr | ( | self | ) |
def assert_exprs | ( | self, | |
* | args | ||
) |
Assert constraints into the goal. >>> x = Int('x') >>> g = Goal() >>> g.assert_exprs(x > 0, x < 2) >>> g [x > 0, x < 2]
Definition at line 5295 of file z3py.py.
Referenced by Goal.add(), Solver.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), Solver.insert(), and Fixedpoint.insert().
def convert_model | ( | self, | |
model | |||
) |
Retrieve model from a satisfiable goal >>> a, b = Ints('a b') >>> g = Goal() >>> g.add(Or(a == 0, a == 1), Or(b == 0, b == 1), a > b) >>> t = Then(Tactic('split-clause'), Tactic('solve-eqs')) >>> r = t(g) >>> r[0] [Or(b == 0, b == 1), Not(0 <= b)] >>> r[1] [Or(b == 0, b == 1), Not(1 <= b)] >>> # Remark: the subgoal r[0] is unsatisfiable >>> # Creating a solver for solving the second subgoal >>> s = Solver() >>> s.add(r[1]) >>> s.check() sat >>> s.model() [b = 0] >>> # Model s.model() does not assign a value to `a` >>> # It is a model for subgoal `r[1]`, but not for goal `g` >>> # The method convert_model creates a model for `g` from a model for `r[1]`. >>> r[1].convert_model(s.model()) [b = 0, a = 1]
Definition at line 5343 of file z3py.py.
def depth | ( | self | ) |
Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`. >>> x, y = Ints('x y') >>> g = Goal() >>> g.add(x == 0, y >= x + 1) >>> g.depth() 0 >>> r = Then('simplify', 'solve-eqs')(g) >>> # r has 1 subgoal >>> len(r) 1 >>> r[0].depth() 2
def dimacs | ( | self | ) |
def get | ( | self, | |
i | |||
) |
Return a constraint in the goal `self`. >>> g = Goal() >>> x, y = Ints('x y') >>> g.add(x == 0, y > x) >>> g.get(0) x == 0 >>> g.get(1) y > x
Definition at line 5267 of file z3py.py.
Referenced by Goal.__getitem__(), and Goal.as_expr().
def inconsistent | ( | self | ) |
Return `True` if `self` contains the `False` constraints. >>> x, y = Ints('x y') >>> g = Goal() >>> g.inconsistent() False >>> g.add(x == 0, x == 1) >>> g [x == 0, x == 1] >>> g.inconsistent() False >>> g2 = Tactic('propagate-values')(g)[0] >>> g2.inconsistent() True
Definition at line 5193 of file z3py.py.
def insert | ( | self, | |
* | args | ||
) |
Add constraints. >>> x = Int('x') >>> g = Goal() >>> g.insert(x > 0, x < 2) >>> g [x > 0, x < 2]
def prec | ( | self | ) |
Return the precision (under-approximation, over-approximation, or precise) of the goal `self`. >>> g = Goal() >>> g.prec() == Z3_GOAL_PRECISE True >>> x, y = Ints('x y') >>> g.add(x == y + 1) >>> g.prec() == Z3_GOAL_PRECISE True >>> t = With(Tactic('add-bounds'), add_bound_lower=0, add_bound_upper=10) >>> g2 = t(g)[0] >>> g2 [x == y + 1, x <= 10, x >= 0, y <= 10, y >= 0] >>> g2.prec() == Z3_GOAL_PRECISE False >>> g2.prec() == Z3_GOAL_UNDER True
Definition at line 5211 of file z3py.py.
Referenced by Goal.precision().
def precision | ( | self | ) |
def sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the goal.
Definition at line 5375 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
def simplify | ( | self, | |
* | arguments, | ||
** | keywords | ||
) |
def size | ( | self | ) |
Return the number of constraints in the goal `self`. >>> g = Goal() >>> g.size() 0 >>> x, y = Ints('x y') >>> g.add(x == 0, y > x) >>> g.size() 2
Definition at line 5241 of file z3py.py.
Referenced by Goal.__len__().
def translate | ( | self, | |
target | |||
) |
Copy goal `self` to context `target`. >>> x = Int('x') >>> g = Goal() >>> g.add(x > 10) >>> g [x > 10] >>> c2 = Context() >>> g2 = g.translate(c2) >>> g2 [x > 10] >>> g.ctx == main_ctx() True >>> g2.ctx == c2 True >>> g2.ctx == main_ctx() False
Definition at line 5383 of file z3py.py.
Referenced by Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().
ctx |
Definition at line 5163 of file z3py.py.
Referenced by Probe.__call__(), AstMap.__contains__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__deepcopy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Goal.__del__(), AstVector.__del__(), AstMap.__del__(), FuncEntry.__del__(), FuncInterp.__del__(), ModelRef.__del__(), Statistics.__del__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), AstMap.__repr__(), Statistics.__repr__(), AstVector.__setitem__(), AstMap.__setitem__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Optimize.check(), Solver.consequences(), Goal.convert_model(), ModelRef.decls(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), ModelRef.get_sort(), ModelRef.get_universe(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.pop(), Optimize.pop(), Goal.prec(), Solver.proof(), AstVector.push(), Solver.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Goal.size(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), Goal.translate(), AstVector.translate(), FuncInterp.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), and FuncEntry.value().
goal |
Definition at line 5164 of file z3py.py.
Referenced by Goal.__deepcopy__(), Goal.__del__(), Goal.assert_exprs(), Goal.convert_model(), Goal.depth(), Goal.dimacs(), Goal.get(), Goal.inconsistent(), Goal.prec(), Goal.sexpr(), Goal.size(), and Goal.translate().