Public Member Functions | |
def | __init__ |
def | __deepcopy__ |
def | __del__ |
def | solver |
def | apply |
def | __call__ |
def | help |
def | param_descrs |
Data Fields | |
ctx | |
tactic | |
Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver(). Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
def __init__ | ( | self, | |
tactic, | |||
ctx = None |
|||
) |
Definition at line 7613 of file z3py.py.
def __del__ | ( | self | ) |
def __call__ | ( | self, | |
goal, | |||
arguments, | |||
keywords | |||
) |
def __deepcopy__ | ( | self, | |
memo = {} |
|||
) |
Definition at line 7627 of file z3py.py.
def apply | ( | self, | |
goal, | |||
arguments, | |||
keywords | |||
) |
Apply tactic `self` to the given goal or Z3 Boolean expression using the given options. >>> x, y = Ints('x y') >>> t = Tactic('solve-eqs') >>> t.apply(And(x == 0, y >= x + 1)) [[y >= 1]]
Definition at line 7651 of file z3py.py.
Referenced by Tactic.__call__().
def help | ( | self | ) |
Display a string containing a description of the available options for the `self` tactic.
Definition at line 7678 of file z3py.py.
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 7682 of file z3py.py.
def solver | ( | self | ) |
Create a solver using the tactic `self`. The solver supports the methods `push()` and `pop()`, but it will always solve each `check()` from scratch. >>> t = Then('simplify', 'nlsat') >>> s = t.solver() >>> x = Real('x') >>> s.add(x**2 == 2, x > 0) >>> s.check() sat >>> s.model() [x = 1.4142135623?]
Definition at line 7634 of file z3py.py.
ctx |
Definition at line 7614 of file z3py.py.
Referenced by Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), Tactic.param_descrs(), and Tactic.solver().
tactic |
Definition at line 7615 of file z3py.py.
Referenced by Tactic.__deepcopy__(), Tactic.__del__(), Tactic.apply(), Tactic.help(), Tactic.param_descrs(), and Tactic.solver().