Public Member Functions | |
def | __init__ (self, tactic, ctx=None) |
def | __del__ (self) |
def | solver (self) |
def | apply (self, goal, arguments, keywords) |
def | __call__ (self, goal, arguments, keywords) |
def | help (self) |
def | param_descrs (self) |
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 6951 of file z3py.py.
def __del__ | ( | self | ) |
def __call__ | ( | self, | |
goal, | |||
arguments, | |||
keywords | |||
) |
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 6986 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.
def param_descrs | ( | self | ) |
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 6969 of file z3py.py.
ctx |
Definition at line 6952 of file z3py.py.
Referenced by Probe.__call__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), Tactic.help(), Tactic.param_descrs(), and Tactic.solver().
tactic |
Definition at line 6953 of file z3py.py.
Referenced by Tactic.__del__(), Tactic.apply(), Tactic.help(), Tactic.param_descrs(), and Tactic.solver().