|
def | __init__ (self, solver=None, ctx=None, logFile=None) |
|
def | __del__ (self) |
|
def | set (self, *args, **keys) |
|
def | push (self) |
|
def | pop (self, num=1) |
|
def | num_scopes (self) |
|
def | reset (self) |
|
def | assert_exprs (self, *args) |
|
def | add (self, *args) |
|
def | __iadd__ (self, fml) |
|
def | append (self, *args) |
|
def | insert (self, *args) |
|
def | assert_and_track (self, a, p) |
|
def | check (self, *assumptions) |
|
def | model (self) |
|
def | import_model_converter (self, other) |
|
def | unsat_core (self) |
|
def | consequences (self, assumptions, variables) |
|
def | from_file (self, filename) |
|
def | from_string (self, s) |
|
def | cube (self, vars=None) |
|
def | cube_vars (self) |
|
def | proof (self) |
|
def | assertions (self) |
|
def | units (self) |
|
def | non_units (self) |
|
def | trail_levels (self) |
|
def | trail (self) |
|
def | statistics (self) |
|
def | reason_unknown (self) |
|
def | help (self) |
|
def | param_descrs (self) |
|
def | __repr__ (self) |
|
def | translate (self, target) |
|
def | __copy__ (self) |
|
def | __deepcopy__ (self, memo={}) |
|
def | sexpr (self) |
|
def | dimacs (self, include_names=True) |
|
def | to_smt2 (self) |
|
def | use_pp (self) |
|
Solver API provides methods for implementing the main SMT 2.0 commands:
push, pop, check, get-model, etc.
Definition at line 6860 of file z3py.py.
◆ __init__()
def __init__ |
( |
|
self, |
|
|
|
solver = None , |
|
|
|
ctx = None , |
|
|
|
logFile = None |
|
) |
| |
Definition at line 6866 of file z3py.py.
6866 def __init__(self, solver=None, ctx=None, logFile=None):
6867 assert solver
is None or ctx
is not None
6868 self.ctx = _get_ctx(ctx)
6869 self.backtrack_level = 4000000000
6874 self.solver = solver
6876 if logFile
is not None:
6877 self.set(
"smtlib2_log", logFile)
◆ __del__()
Definition at line 6879 of file z3py.py.
6880 if self.solver
is not None and self.ctx.ref()
is not None:
◆ __copy__()
Definition at line 7304 of file z3py.py.
7305 return self.translate(self.ctx)
◆ __deepcopy__()
def __deepcopy__ |
( |
|
self, |
|
|
|
memo = {} |
|
) |
| |
Definition at line 7307 of file z3py.py.
7307 def __deepcopy__(self, memo={}):
7308 return self.translate(self.ctx)
◆ __iadd__()
def __iadd__ |
( |
|
self, |
|
|
|
fml |
|
) |
| |
Definition at line 7002 of file z3py.py.
7002 def __iadd__(self, fml):
◆ __repr__()
Return a formatted string with all added constraints.
Definition at line 7287 of file z3py.py.
7288 """Return a formatted string with all added constraints."""
7289 return obj_to_string(self)
◆ add()
Assert constraints into the solver.
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]
Definition at line 6991 of file z3py.py.
6991 def add(self, *args):
6992 """Assert constraints into the solver.
6996 >>> s.add(x > 0, x < 2)
7000 self.assert_exprs(*args)
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
◆ append()
def append |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints into the solver.
>>> x = Int('x')
>>> s = Solver()
>>> s.append(x > 0, x < 2)
>>> s
[x > 0, x < 2]
Definition at line 7006 of file z3py.py.
7006 def append(self, *args):
7007 """Assert constraints into the solver.
7011 >>> s.append(x > 0, x < 2)
7015 self.assert_exprs(*args)
◆ assert_and_track()
def assert_and_track |
( |
|
self, |
|
|
|
a, |
|
|
|
p |
|
) |
| |
Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
If `p` is a string, it will be automatically converted into a Boolean constant.
>>> x = Int('x')
>>> p3 = Bool('p3')
>>> s = Solver()
>>> s.set(unsat_core=True)
>>> s.assert_and_track(x > 0, 'p1')
>>> s.assert_and_track(x != 1, 'p2')
>>> s.assert_and_track(x < 0, p3)
>>> print(s.check())
unsat
>>> c = s.unsat_core()
>>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True
Definition at line 7028 of file z3py.py.
7028 def assert_and_track(self, a, p):
7029 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
7031 If `p` is a string, it will be automatically converted into a Boolean constant.
7036 >>> s.set(unsat_core=True)
7037 >>> s.assert_and_track(x > 0, 'p1')
7038 >>> s.assert_and_track(x != 1, 'p2')
7039 >>> s.assert_and_track(x < 0, p3)
7040 >>> print(s.check())
7042 >>> c = s.unsat_core()
7052 if isinstance(p, str):
7053 p =
Bool(p, self.ctx)
7054 _z3_assert(isinstance(a, BoolRef),
"Boolean expression expected")
7055 _z3_assert(isinstance(p, BoolRef)
and is_const(p),
"Boolean expression expected")
◆ assert_exprs()
def assert_exprs |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints into the solver.
>>> x = Int('x')
>>> s = Solver()
>>> s.assert_exprs(x > 0, x < 2)
>>> s
[x > 0, x < 2]
Definition at line 6972 of file z3py.py.
6972 def assert_exprs(self, *args):
6973 """Assert constraints into the solver.
6977 >>> s.assert_exprs(x > 0, x < 2)
6981 args = _get_args(args)
6984 if isinstance(arg, Goal)
or isinstance(arg, AstVector):
Referenced by Solver.add(), Fixedpoint.add(), Optimize.add(), Solver.append(), Fixedpoint.append(), Solver.insert(), and Fixedpoint.insert().
◆ assertions()
Return an AST vector containing all added constraints.
>>> s = Solver()
>>> s.assertions()
[]
>>> a = Int('a')
>>> s.add(a > 0)
>>> s.add(a < 10)
>>> s.assertions()
[a > 0, a < 10]
Definition at line 7211 of file z3py.py.
7211 def assertions(self):
7212 """Return an AST vector containing all added constraints.
Referenced by Solver.to_smt2().
◆ check()
def check |
( |
|
self, |
|
|
* |
assumptions |
|
) |
| |
Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
>>> x = Int('x')
>>> s = Solver()
>>> s.check()
sat
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> s.model().eval(x)
1
>>> s.add(x < 1)
>>> s.check()
unsat
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown
Definition at line 7058 of file z3py.py.
7058 def check(self, *assumptions):
7059 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
7065 >>> s.add(x > 0, x < 2)
7068 >>> s.model().eval(x)
7074 >>> s.add(2**x == 4)
7079 assumptions = _get_args(assumptions)
7080 num = len(assumptions)
7081 _assumptions = (Ast * num)()
7082 for i
in range(num):
7083 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7085 return CheckSatResult(r)
◆ consequences()
def consequences |
( |
|
self, |
|
|
|
assumptions, |
|
|
|
variables |
|
) |
| |
Determine fixed values for the variables based on the solver state and assumptions.
>>> s = Solver()
>>> a, b, c, d = Bools('a b c d')
>>> s.add(Implies(a,b), Implies(b, c))
>>> s.consequences([a],[b,c,d])
(sat, [Implies(a, b), Implies(a, c)])
>>> s.consequences([Not(c),d],[a,b,c,d])
(sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
Definition at line 7142 of file z3py.py.
7142 def consequences(self, assumptions, variables):
7143 """Determine fixed values for the variables based on the solver state and assumptions.
7145 >>> a, b, c, d = Bools('a b c d')
7146 >>> s.add(Implies(a,b), Implies(b, c))
7147 >>> s.consequences([a],[b,c,d])
7148 (sat, [Implies(a, b), Implies(a, c)])
7149 >>> s.consequences([Not(c),d],[a,b,c,d])
7150 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7152 if isinstance(assumptions, list):
7153 _asms = AstVector(
None, self.ctx)
7154 for a
in assumptions:
7157 if isinstance(variables, list):
7158 _vars = AstVector(
None, self.ctx)
7162 _z3_assert(isinstance(assumptions, AstVector),
"ast vector expected")
7163 _z3_assert(isinstance(variables, AstVector),
"ast vector expected")
7164 consequences = AstVector(
None, self.ctx)
7166 variables.vector, consequences.vector)
7167 sz = len(consequences)
7168 consequences = [consequences[i]
for i
in range(sz)]
7169 return CheckSatResult(r), consequences
◆ cube()
def cube |
( |
|
self, |
|
|
|
vars = None |
|
) |
| |
Get set of cubes
The method takes an optional set of variables that restrict which
variables may be used as a starting point for cubing.
If vars is not None, then the first case split is based on a variable in
this set.
Definition at line 7179 of file z3py.py.
7179 def cube(self, vars=None):
7181 The method takes an optional set of variables that restrict which
7182 variables may be used as a starting point for cubing.
7183 If vars is not None, then the first case split is based on a variable in
7186 self.cube_vs = AstVector(
None, self.ctx)
7187 if vars
is not None:
7189 self.cube_vs.
push(v)
7191 lvl = self.backtrack_level
7192 self.backtrack_level = 4000000000
7193 r = AstVector(
Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7194 if (len(r) == 1
and is_false(r[0])):
◆ cube_vars()
Access the set of variables that were touched by the most recently generated cube.
This set of variables can be used as a starting point for additional cubes.
The idea is that variables that appear in clauses that are reduced by the most recent
cube are likely more useful to cube on.
Definition at line 7200 of file z3py.py.
7200 def cube_vars(self):
7201 """Access the set of variables that were touched by the most recently generated cube.
7202 This set of variables can be used as a starting point for additional cubes.
7203 The idea is that variables that appear in clauses that are reduced by the most recent
7204 cube are likely more useful to cube on."""
◆ dimacs()
def dimacs |
( |
|
self, |
|
|
|
include_names = True |
|
) |
| |
Return a textual representation of the solver in DIMACS format.
Definition at line 7322 of file z3py.py.
7322 def dimacs(self, include_names=True):
7323 """Return a textual representation of the solver in DIMACS format."""
◆ from_file()
def from_file |
( |
|
self, |
|
|
|
filename |
|
) |
| |
Parse assertions from a file
Definition at line 7171 of file z3py.py.
7171 def from_file(self, filename):
7172 """Parse assertions from a file"""
◆ from_string()
def from_string |
( |
|
self, |
|
|
|
s |
|
) |
| |
Parse assertions from a string
Definition at line 7175 of file z3py.py.
7175 def from_string(self, s):
7176 """Parse assertions from a string"""
◆ help()
Display a string describing all available options.
Definition at line 7279 of file z3py.py.
7280 """Display a string describing all available options."""
◆ import_model_converter()
def import_model_converter |
( |
|
self, |
|
|
|
other |
|
) |
| |
Import model converter from other into the current solver
Definition at line 7106 of file z3py.py.
7106 def import_model_converter(self, other):
7107 """Import model converter from other into the current solver"""
◆ insert()
def insert |
( |
|
self, |
|
|
* |
args |
|
) |
| |
Assert constraints into the solver.
>>> x = Int('x')
>>> s = Solver()
>>> s.insert(x > 0, x < 2)
>>> s
[x > 0, x < 2]
Definition at line 7017 of file z3py.py.
7017 def insert(self, *args):
7018 """Assert constraints into the solver.
7022 >>> s.insert(x > 0, x < 2)
7026 self.assert_exprs(*args)
◆ model()
Return a model for the last `check()`.
This function raises an exception if
a model is not available (e.g., last `check()` returned unsat).
>>> s = Solver()
>>> a = Int('a')
>>> s.add(a + 2 == 0)
>>> s.check()
sat
>>> s.model()
[a = -2]
Definition at line 7087 of file z3py.py.
7088 """Return a model for the last `check()`.
7090 This function raises an exception if
7091 a model is not available (e.g., last `check()` returned unsat).
7095 >>> s.add(a + 2 == 0)
7104 raise Z3Exception(
"model is not available")
Referenced by FuncInterp.translate().
◆ non_units()
Return an AST vector containing all atomic formulas in solver state that are not units.
Definition at line 7230 of file z3py.py.
7230 def non_units(self):
7231 """Return an AST vector containing all atomic formulas in solver state that are not units.
◆ num_scopes()
Return the current number of backtracking points.
>>> s = Solver()
>>> s.num_scopes()
0
>>> s.push()
>>> s.num_scopes()
1
>>> s.push()
>>> s.num_scopes()
2
>>> s.pop()
>>> s.num_scopes()
1
Definition at line 6940 of file z3py.py.
6940 def num_scopes(self):
6941 """Return the current number of backtracking points.
◆ param_descrs()
Return the parameter description set.
Definition at line 7283 of file z3py.py.
7283 def param_descrs(self):
7284 """Return the parameter description set."""
◆ pop()
def pop |
( |
|
self, |
|
|
|
num = 1 |
|
) |
| |
Backtrack \\c num backtracking points.
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]
Definition at line 6918 of file z3py.py.
6918 def pop(self, num=1):
6919 """Backtrack \\c num backtracking points.
◆ proof()
Return a proof for the last `check()`. Proof construction must be enabled.
Definition at line 7207 of file z3py.py.
7208 """Return a proof for the last `check()`. Proof construction must be enabled."""
◆ push()
Create a backtracking point.
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.push()
>>> s.add(x < 1)
>>> s
[x > 0, x < 1]
>>> s.check()
unsat
>>> s.pop()
>>> s.check()
sat
>>> s
[x > 0]
Definition at line 6896 of file z3py.py.
6897 """Create a backtracking point.
◆ reason_unknown()
def reason_unknown |
( |
|
self | ) |
|
Return a string describing why the last `check()` returned `unknown`.
>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(2**x == 4)
>>> s.check()
unknown
>>> s.reason_unknown()
'(incomplete (theory arithmetic))'
Definition at line 7266 of file z3py.py.
7266 def reason_unknown(self):
7267 """Return a string describing why the last `check()` returned `unknown`.
7270 >>> s = SimpleSolver()
7271 >>> s.add(2**x == 4)
7274 >>> s.reason_unknown()
7275 '(incomplete (theory arithmetic))'
◆ reset()
Remove all asserted constraints and backtracking points created using `push()`.
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s
[x > 0]
>>> s.reset()
>>> s
[]
Definition at line 6958 of file z3py.py.
6959 """Remove all asserted constraints and backtracking points created using `push()`.
◆ set()
def set |
( |
|
self, |
|
|
* |
args, |
|
|
** |
keys |
|
) |
| |
Set a configuration option.
The method `help()` return a string containing all available options.
>>> s = Solver()
>>> # The option MBQI can be set using three different approaches.
>>> s.set(mbqi=True)
>>> s.set('MBQI', True)
>>> s.set(':mbqi', True)
Definition at line 6883 of file z3py.py.
6883 def set(self, *args, **keys):
6884 """Set a configuration option.
6885 The method `help()` return a string containing all available options.
6888 >>> # The option MBQI can be set using three different approaches.
6889 >>> s.set(mbqi=True)
6890 >>> s.set('MBQI', True)
6891 >>> s.set(':mbqi', True)
◆ sexpr()
Return a formatted string (in Lisp-like format) with all added constraints.
We say the string is in s-expression format.
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0)
>>> s.add(x < 2)
>>> r = s.sexpr()
Definition at line 7310 of file z3py.py.
7311 """Return a formatted string (in Lisp-like format) with all added constraints.
7312 We say the string is in s-expression format.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
◆ statistics()
Return statistics for the last `check()`.
>>> s = SimpleSolver()
>>> x = Int('x')
>>> s.add(x > 0)
>>> s.check()
sat
>>> st = s.statistics()
>>> st.get_key_value('final checks')
1
>>> len(st) > 0
True
>>> st[0] != 0
True
Definition at line 7248 of file z3py.py.
7248 def statistics(self):
7249 """Return statistics for the last `check()`.
7251 >>> s = SimpleSolver()
7256 >>> st = s.statistics()
7257 >>> st.get_key_value('final checks')
◆ to_smt2()
return SMTLIB2 formatted benchmark for solver's assertions
Definition at line 7326 of file z3py.py.
7327 """return SMTLIB2 formatted benchmark for solver's assertions"""
7328 es = self.assertions()
7334 for i
in range(sz1):
7335 v[i] = es[i].as_ast()
7337 e = es[sz1].as_ast()
7339 e =
BoolVal(
True, self.ctx).as_ast()
7341 self.ctx.ref(),
"benchmark generated from python API",
"",
"unknown",
"", sz1, v, e,
◆ trail()
Return trail of the solver state after a check() call.
Definition at line 7243 of file z3py.py.
7244 """Return trail of the solver state after a check() call.
Referenced by Solver.trail_levels().
◆ trail_levels()
Return trail and decision levels of the solver state after a check() call.
Definition at line 7235 of file z3py.py.
7235 def trail_levels(self):
7236 """Return trail and decision levels of the solver state after a check() call.
7238 trail = self.trail()
7239 levels = (ctypes.c_uint * len(trail))()
7241 return trail, levels
◆ translate()
def translate |
( |
|
self, |
|
|
|
target |
|
) |
| |
Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
>>> c1 = Context()
>>> c2 = Context()
>>> s1 = Solver(ctx=c1)
>>> s2 = s1.translate(c2)
Definition at line 7291 of file z3py.py.
7291 def translate(self, target):
7292 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7296 >>> s1 = Solver(ctx=c1)
7297 >>> s2 = s1.translate(c2)
7300 _z3_assert(isinstance(target, Context),
"argument must be a Z3 context")
7302 return Solver(solver, target)
Referenced by Solver.__copy__(), and Solver.__deepcopy__().
◆ units()
Return an AST vector containing all currently inferred units.
Definition at line 7225 of file z3py.py.
7226 """Return an AST vector containing all currently inferred units.
◆ unsat_core()
Return a subset (as an AST vector) of the assumptions provided to the last check().
These are the assumptions Z3 used in the unsatisfiability proof.
Assumptions are available in Z3. They are used to extract unsatisfiable cores.
They may be also used to "retract" assumptions. Note that, assumptions are not really
"soft constraints", but they can be used to implement them.
>>> p1, p2, p3 = Bools('p1 p2 p3')
>>> x, y = Ints('x y')
>>> s = Solver()
>>> s.add(Implies(p1, x > 0))
>>> s.add(Implies(p2, y > x))
>>> s.add(Implies(p2, y < 1))
>>> s.add(Implies(p3, y > -3))
>>> s.check(p1, p2, p3)
unsat
>>> core = s.unsat_core()
>>> len(core)
2
>>> p1 in core
True
>>> p2 in core
True
>>> p3 in core
False
>>> # "Retracting" p2
>>> s.check(p1, p3)
sat
Definition at line 7110 of file z3py.py.
7110 def unsat_core(self):
7111 """Return a subset (as an AST vector) of the assumptions provided to the last check().
7113 These are the assumptions Z3 used in the unsatisfiability proof.
7114 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7115 They may be also used to "retract" assumptions. Note that, assumptions are not really
7116 "soft constraints", but they can be used to implement them.
7118 >>> p1, p2, p3 = Bools('p1 p2 p3')
7119 >>> x, y = Ints('x y')
7121 >>> s.add(Implies(p1, x > 0))
7122 >>> s.add(Implies(p2, y > x))
7123 >>> s.add(Implies(p2, y < 1))
7124 >>> s.add(Implies(p3, y > -3))
7125 >>> s.check(p1, p2, p3)
7127 >>> core = s.unsat_core()
7136 >>> # "Retracting" p2
◆ backtrack_level
◆ ctx
Definition at line 6868 of file z3py.py.
Referenced by Probe.__call__(), Solver.__copy__(), Solver.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Solver.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Solver.assert_and_track(), Optimize.assert_and_track(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), UserPropagateBase.ctx_ref(), Solver.dimacs(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Solver.help(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Solver.import_model_converter(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), Solver.non_units(), Solver.num_scopes(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Solver.pop(), Optimize.pop(), Solver.proof(), Solver.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Solver.reset(), Solver.set(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), and Fixedpoint.update_rule().
◆ cube_vs
◆ solver
Definition at line 6870 of file z3py.py.
Referenced by Solver.__del__(), UserPropagateBase.add(), UserPropagateBase.add_diseq(), UserPropagateBase.add_eq(), UserPropagateBase.add_final(), UserPropagateBase.add_fixed(), Solver.assert_and_track(), Solver.assert_exprs(), Solver.assertions(), Solver.check(), Solver.consequences(), UserPropagateBase.ctx(), Solver.dimacs(), Solver.from_file(), Solver.from_string(), Solver.help(), Solver.import_model_converter(), Solver.model(), Solver.non_units(), Solver.num_scopes(), Solver.param_descrs(), Solver.pop(), Solver.proof(), Solver.push(), Solver.reason_unknown(), Solver.reset(), Solver.set(), Solver.sexpr(), Solver.statistics(), Solver.trail(), Solver.trail_levels(), Solver.translate(), Solver.units(), and Solver.unsat_core().
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.
Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target)
Copy a solver s from the context source to the context target.
def __init__(self, s, ctx=None)
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.
Z3_ast Z3_API Z3_solver_get_proof(Z3_context c, Z3_solver s)
Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions.
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[])
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat c...
expr range(expr const &lo, expr const &hi)
void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p)
Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.
def pop(self, num_scopes)
Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s)
Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions.
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c, Z3_solver s, Z3_ast_vector assumptions, Z3_ast_vector variables, Z3_ast_vector consequences)
retrieve consequences from solver that determine values of the supplied function symbols.
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
Create a backtracking point.
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.
Z3_lbool Z3_API Z3_solver_check_assumptions(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[])
Check whether the assertions in the given solver and optional assumptions are consistent or not.
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.
void Z3_API Z3_solver_import_model_converter(Z3_context ctx, Z3_solver src, Z3_solver dst)
Ad-hoc method for importing model conversion from solver.
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.
Z3_string Z3_API Z3_solver_get_reason_unknown(Z3_context c, Z3_solver s)
Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_ch...
Z3_ast_vector Z3_API Z3_solver_get_trail(Z3_context c, Z3_solver s)
Return the trail modulo model conversion, in order of decision level The decision level can be retrie...
def BoolVal(val, ctx=None)
Z3_string Z3_API Z3_benchmark_to_smtlib_string(Z3_context c, Z3_string name, Z3_string logic, Z3_string status, Z3_string attributes, unsigned num_assumptions, Z3_ast const assumptions[], Z3_ast formula)
Convert the given benchmark into SMT-LIB formatted string.
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.
Z3_solver Z3_API Z3_mk_solver(Z3_context c)
Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally ...
Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s)
Return the set of non units in the solver state.
Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s)
Return the parameter description set for the given solver object.
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s)
Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the as...
Z3_ast_vector Z3_API Z3_solver_cube(Z3_context c, Z3_solver s, Z3_ast_vector vars, unsigned backtrack_level)
extract a next cube for a solver. The last cube is the constant true or false. The number of (non-con...
Z3_string Z3_API Z3_solver_to_dimacs_string(Z3_context c, Z3_solver s, bool include_names)
Convert a solver into a DIMACS formatted string.
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.
def args2params(arguments, keywords, ctx=None)
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.