Z3
Public Member Functions | Data Fields
Solver Class Reference
+ Inheritance diagram for Solver:

Public Member Functions

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)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 ctx
 
 backtrack_level
 
 solver
 
 cube_vs
 

Detailed Description

Solver API provides methods for implementing the main SMT 2.0 commands:
push, pop, check, get-model, etc.

Definition at line 6787 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  solver = None,
  ctx = None,
  logFile = None 
)

Definition at line 6793 of file z3py.py.

6793 def __init__(self, solver=None, ctx=None, logFile=None):
6794 assert solver is None or ctx is not None
6795 self.ctx = _get_ctx(ctx)
6796 self.backtrack_level = 4000000000
6797 self.solver = None
6798 if solver is None:
6799 self.solver = Z3_mk_solver(self.ctx.ref())
6800 else:
6801 self.solver = solver
6802 Z3_solver_inc_ref(self.ctx.ref(), self.solver)
6803 if logFile is not None:
6804 self.set("smtlib2_log", logFile)
6805
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 ...
void Z3_API Z3_solver_inc_ref(Z3_context c, Z3_solver s)
Increment the reference counter of the given solver.

◆ __del__()

def __del__ (   self)

Definition at line 6806 of file z3py.py.

6806 def __del__(self):
6807 if self.solver is not None and self.ctx.ref() is not None:
6808 Z3_solver_dec_ref(self.ctx.ref(), self.solver)
6809
void Z3_API Z3_solver_dec_ref(Z3_context c, Z3_solver s)
Decrement the reference counter of the given solver.

Member Function Documentation

◆ __copy__()

def __copy__ (   self)

Definition at line 7231 of file z3py.py.

7231 def __copy__(self):
7232 return self.translate(self.ctx)
7233

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 7234 of file z3py.py.

7234 def __deepcopy__(self, memo={}):
7235 return self.translate(self.ctx)
7236

◆ __iadd__()

def __iadd__ (   self,
  fml 
)

Definition at line 6929 of file z3py.py.

6929 def __iadd__(self, fml):
6930 self.add(fml)
6931 return self
6932

◆ __repr__()

def __repr__ (   self)
Return a formatted string with all added constraints.

Definition at line 7214 of file z3py.py.

7214 def __repr__(self):
7215 """Return a formatted string with all added constraints."""
7216 return obj_to_string(self)
7217

◆ add()

def add (   self,
args 
)
Assert constraints into the solver.

>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s
[x > 0, x < 2]

Definition at line 6918 of file z3py.py.

6918 def add(self, *args):
6919 """Assert constraints into the solver.
6920
6921 >>> x = Int('x')
6922 >>> s = Solver()
6923 >>> s.add(x > 0, x < 2)
6924 >>> s
6925 [x > 0, x < 2]
6926 """
6927 self.assert_exprs(*args)
6928
def Int(name, ctx=None)
Definition: z3py.py:3210

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 6933 of file z3py.py.

6933 def append(self, *args):
6934 """Assert constraints into the solver.
6935
6936 >>> x = Int('x')
6937 >>> s = Solver()
6938 >>> s.append(x > 0, x < 2)
6939 >>> s
6940 [x > 0, x < 2]
6941 """
6942 self.assert_exprs(*args)
6943

◆ 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 6955 of file z3py.py.

6955 def assert_and_track(self, a, p):
6956 """Assert constraint `a` and track it in the unsat core using the Boolean constant `p`.
6957
6958 If `p` is a string, it will be automatically converted into a Boolean constant.
6959
6960 >>> x = Int('x')
6961 >>> p3 = Bool('p3')
6962 >>> s = Solver()
6963 >>> s.set(unsat_core=True)
6964 >>> s.assert_and_track(x > 0, 'p1')
6965 >>> s.assert_and_track(x != 1, 'p2')
6966 >>> s.assert_and_track(x < 0, p3)
6967 >>> print(s.check())
6968 unsat
6969 >>> c = s.unsat_core()
6970 >>> len(c)
6971 2
6972 >>> Bool('p1') in c
6973 True
6974 >>> Bool('p2') in c
6975 False
6976 >>> p3 in c
6977 True
6978 """
6979 if isinstance(p, str):
6980 p = Bool(p, self.ctx)
6981 _z3_assert(isinstance(a, BoolRef), "Boolean expression expected")
6982 _z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
6983 Z3_solver_assert_and_track(self.ctx.ref(), self.solver, a.as_ast(), p.as_ast())
6984
def is_const(a)
Definition: z3py.py:1259
def Bool(name, ctx=None)
Definition: z3py.py:1692
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.

◆ 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 6899 of file z3py.py.

6899 def assert_exprs(self, *args):
6900 """Assert constraints into the solver.
6901
6902 >>> x = Int('x')
6903 >>> s = Solver()
6904 >>> s.assert_exprs(x > 0, x < 2)
6905 >>> s
6906 [x > 0, x < 2]
6907 """
6908 args = _get_args(args)
6909 s = BoolSort(self.ctx)
6910 for arg in args:
6911 if isinstance(arg, Goal) or isinstance(arg, AstVector):
6912 for f in arg:
6913 Z3_solver_assert(self.ctx.ref(), self.solver, f.as_ast())
6914 else:
6915 arg = s.cast(arg)
6916 Z3_solver_assert(self.ctx.ref(), self.solver, arg.as_ast())
6917
def BoolSort(ctx=None)
Definition: z3py.py:1655
void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a)
Assert a constraint into the solver.

Referenced by Goal.add(), Solver.add(), Fixedpoint.add(), Optimize.add(), Goal.append(), Solver.append(), Fixedpoint.append(), Goal.insert(), Solver.insert(), and Fixedpoint.insert().

◆ assertions()

def assertions (   self)
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 7138 of file z3py.py.

7138 def assertions(self):
7139 """Return an AST vector containing all added constraints.
7140
7141 >>> s = Solver()
7142 >>> s.assertions()
7143 []
7144 >>> a = Int('a')
7145 >>> s.add(a > 0)
7146 >>> s.add(a < 10)
7147 >>> s.assertions()
7148 [a > 0, a < 10]
7149 """
7150 return AstVector(Z3_solver_get_assertions(self.ctx.ref(), self.solver), self.ctx)
7151
Z3_ast_vector Z3_API Z3_solver_get_assertions(Z3_context c, Z3_solver s)
Return the set of asserted formulas on the solver.

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 6985 of file z3py.py.

6985 def check(self, *assumptions):
6986 """Check whether the assertions in the given solver plus the optional assumptions are consistent or not.
6987
6988 >>> x = Int('x')
6989 >>> s = Solver()
6990 >>> s.check()
6991 sat
6992 >>> s.add(x > 0, x < 2)
6993 >>> s.check()
6994 sat
6995 >>> s.model().eval(x)
6996 1
6997 >>> s.add(x < 1)
6998 >>> s.check()
6999 unsat
7000 >>> s.reset()
7001 >>> s.add(2**x == 4)
7002 >>> s.check()
7003 unknown
7004 """
7005 s = BoolSort(self.ctx)
7006 assumptions = _get_args(assumptions)
7007 num = len(assumptions)
7008 _assumptions = (Ast * num)()
7009 for i in range(num):
7010 _assumptions[i] = s.cast(assumptions[i]).as_ast()
7011 r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
7012 return CheckSatResult(r)
7013
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
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.

Referenced by Solver.model().

◆ 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 7069 of file z3py.py.

7069 def consequences(self, assumptions, variables):
7070 """Determine fixed values for the variables based on the solver state and assumptions.
7071 >>> s = Solver()
7072 >>> a, b, c, d = Bools('a b c d')
7073 >>> s.add(Implies(a,b), Implies(b, c))
7074 >>> s.consequences([a],[b,c,d])
7075 (sat, [Implies(a, b), Implies(a, c)])
7076 >>> s.consequences([Not(c),d],[a,b,c,d])
7077 (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
7078 """
7079 if isinstance(assumptions, list):
7080 _asms = AstVector(None, self.ctx)
7081 for a in assumptions:
7082 _asms.push(a)
7083 assumptions = _asms
7084 if isinstance(variables, list):
7085 _vars = AstVector(None, self.ctx)
7086 for a in variables:
7087 _vars.push(a)
7088 variables = _vars
7089 _z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
7090 _z3_assert(isinstance(variables, AstVector), "ast vector expected")
7091 consequences = AstVector(None, self.ctx)
7092 r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
7093 variables.vector, consequences.vector)
7094 sz = len(consequences)
7095 consequences = [consequences[i] for i in range(sz)]
7096 return CheckSatResult(r), consequences
7097
def Bools(names, ctx=None)
Definition: z3py.py:1704
def Not(a, ctx=None)
Definition: z3py.py:1779
def Implies(a, b, ctx=None)
Definition: z3py.py:1749
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.

◆ 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 7106 of file z3py.py.

7106 def cube(self, vars=None):
7107 """Get set of cubes
7108 The method takes an optional set of variables that restrict which
7109 variables may be used as a starting point for cubing.
7110 If vars is not None, then the first case split is based on a variable in
7111 this set.
7112 """
7113 self.cube_vs = AstVector(None, self.ctx)
7114 if vars is not None:
7115 for v in vars:
7116 self.cube_vs.push(v)
7117 while True:
7118 lvl = self.backtrack_level
7119 self.backtrack_level = 4000000000
7120 r = AstVector(Z3_solver_cube(self.ctx.ref(), self.solver, self.cube_vs.vector, lvl), self.ctx)
7121 if (len(r) == 1 and is_false(r[0])):
7122 return
7123 yield r
7124 if (len(r) == 0):
7125 return
7126
def is_false(a)
Definition: z3py.py:1571
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...

◆ cube_vars()

def cube_vars (   self)
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 7127 of file z3py.py.

7127 def cube_vars(self):
7128 """Access the set of variables that were touched by the most recently generated cube.
7129 This set of variables can be used as a starting point for additional cubes.
7130 The idea is that variables that appear in clauses that are reduced by the most recent
7131 cube are likely more useful to cube on."""
7132 return self.cube_vs
7133

◆ dimacs()

def dimacs (   self,
  include_names = True 
)
Return a textual representation of the solver in DIMACS format.

Definition at line 7249 of file z3py.py.

7249 def dimacs(self, include_names=True):
7250 """Return a textual representation of the solver in DIMACS format."""
7251 return Z3_solver_to_dimacs_string(self.ctx.ref(), self.solver, include_names)
7252
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.

◆ from_file()

def from_file (   self,
  filename 
)
Parse assertions from a file

Definition at line 7098 of file z3py.py.

7098 def from_file(self, filename):
7099 """Parse assertions from a file"""
7100 Z3_solver_from_file(self.ctx.ref(), self.solver, filename)
7101
void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a file.

◆ from_string()

def from_string (   self,
  s 
)
Parse assertions from a string

Definition at line 7102 of file z3py.py.

7102 def from_string(self, s):
7103 """Parse assertions from a string"""
7104 Z3_solver_from_string(self.ctx.ref(), self.solver, s)
7105
void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name)
load solver assertions from a string.

◆ help()

def help (   self)
Display a string describing all available options.

Definition at line 7206 of file z3py.py.

7206 def help(self):
7207 """Display a string describing all available options."""
7208 print(Z3_solver_get_help(self.ctx.ref(), self.solver))
7209
Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s)
Return a string describing all solver available parameters.

Referenced by Solver.set().

◆ import_model_converter()

def import_model_converter (   self,
  other 
)
Import model converter from other into the current solver

Definition at line 7033 of file z3py.py.

7033 def import_model_converter(self, other):
7034 """Import model converter from other into the current solver"""
7035 Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver)
7036
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.

◆ 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 6944 of file z3py.py.

6944 def insert(self, *args):
6945 """Assert constraints into the solver.
6946
6947 >>> x = Int('x')
6948 >>> s = Solver()
6949 >>> s.insert(x > 0, x < 2)
6950 >>> s
6951 [x > 0, x < 2]
6952 """
6953 self.assert_exprs(*args)
6954

◆ model()

def model (   self)
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 7014 of file z3py.py.

7014 def model(self):
7015 """Return a model for the last `check()`.
7016
7017 This function raises an exception if
7018 a model is not available (e.g., last `check()` returned unsat).
7019
7020 >>> s = Solver()
7021 >>> a = Int('a')
7022 >>> s.add(a + 2 == 0)
7023 >>> s.check()
7024 sat
7025 >>> s.model()
7026 [a = -2]
7027 """
7028 try:
7029 return ModelRef(Z3_solver_get_model(self.ctx.ref(), self.solver), self.ctx)
7030 except Z3Exception:
7031 raise Z3Exception("model is not available")
7032
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.

Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), ModelRef.sexpr(), FuncInterp.translate(), and ModelRef.translate().

◆ non_units()

def non_units (   self)
Return an AST vector containing all atomic formulas in solver state that are not units.

Definition at line 7157 of file z3py.py.

7157 def non_units(self):
7158 """Return an AST vector containing all atomic formulas in solver state that are not units.
7159 """
7160 return AstVector(Z3_solver_get_non_units(self.ctx.ref(), self.solver), self.ctx)
7161
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.

◆ num_scopes()

def num_scopes (   self)
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 6867 of file z3py.py.

6867 def num_scopes(self):
6868 """Return the current number of backtracking points.
6869
6870 >>> s = Solver()
6871 >>> s.num_scopes()
6872 0
6873 >>> s.push()
6874 >>> s.num_scopes()
6875 1
6876 >>> s.push()
6877 >>> s.num_scopes()
6878 2
6879 >>> s.pop()
6880 >>> s.num_scopes()
6881 1
6882 """
6883 return Z3_solver_get_num_scopes(self.ctx.ref(), self.solver)
6884
unsigned Z3_API Z3_solver_get_num_scopes(Z3_context c, Z3_solver s)
Return the number of backtracking points.

◆ param_descrs()

def param_descrs (   self)
Return the parameter description set.

Definition at line 7210 of file z3py.py.

7210 def param_descrs(self):
7211 """Return the parameter description set."""
7212 return ParamDescrsRef(Z3_solver_get_param_descrs(self.ctx.ref(), self.solver), self.ctx)
7213
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.

◆ 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 6845 of file z3py.py.

6845 def pop(self, num=1):
6846 """Backtrack \\c num backtracking points.
6847
6848 >>> x = Int('x')
6849 >>> s = Solver()
6850 >>> s.add(x > 0)
6851 >>> s
6852 [x > 0]
6853 >>> s.push()
6854 >>> s.add(x < 1)
6855 >>> s
6856 [x > 0, x < 1]
6857 >>> s.check()
6858 unsat
6859 >>> s.pop()
6860 >>> s.check()
6861 sat
6862 >>> s
6863 [x > 0]
6864 """
6865 Z3_solver_pop(self.ctx.ref(), self.solver, num)
6866
void Z3_API Z3_solver_pop(Z3_context c, Z3_solver s, unsigned n)
Backtrack n backtracking points.

◆ proof()

def proof (   self)
Return a proof for the last `check()`. Proof construction must be enabled.

Definition at line 7134 of file z3py.py.

7134 def proof(self):
7135 """Return a proof for the last `check()`. Proof construction must be enabled."""
7136 return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
7137
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.

◆ push()

def push (   self)
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 6823 of file z3py.py.

6823 def push(self):
6824 """Create a backtracking point.
6825
6826 >>> x = Int('x')
6827 >>> s = Solver()
6828 >>> s.add(x > 0)
6829 >>> s
6830 [x > 0]
6831 >>> s.push()
6832 >>> s.add(x < 1)
6833 >>> s
6834 [x > 0, x < 1]
6835 >>> s.check()
6836 unsat
6837 >>> s.pop()
6838 >>> s.check()
6839 sat
6840 >>> s
6841 [x > 0]
6842 """
6843 Z3_solver_push(self.ctx.ref(), self.solver)
6844
void Z3_API Z3_solver_push(Z3_context c, Z3_solver s)
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 7193 of file z3py.py.

7193 def reason_unknown(self):
7194 """Return a string describing why the last `check()` returned `unknown`.
7195
7196 >>> x = Int('x')
7197 >>> s = SimpleSolver()
7198 >>> s.add(2**x == 4)
7199 >>> s.check()
7200 unknown
7201 >>> s.reason_unknown()
7202 '(incomplete (theory arithmetic))'
7203 """
7204 return Z3_solver_get_reason_unknown(self.ctx.ref(), self.solver)
7205
def SimpleSolver(ctx=None, logFile=None)
Definition: z3py.py:7293
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...

◆ reset()

def reset (   self)
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 6885 of file z3py.py.

6885 def reset(self):
6886 """Remove all asserted constraints and backtracking points created using `push()`.
6887
6888 >>> x = Int('x')
6889 >>> s = Solver()
6890 >>> s.add(x > 0)
6891 >>> s
6892 [x > 0]
6893 >>> s.reset()
6894 >>> s
6895 []
6896 """
6897 Z3_solver_reset(self.ctx.ref(), self.solver)
6898
void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s)
Remove all assertions from the solver.

◆ 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 6810 of file z3py.py.

6810 def set(self, *args, **keys):
6811 """Set a configuration option.
6812 The method `help()` return a string containing all available options.
6813
6814 >>> s = Solver()
6815 >>> # The option MBQI can be set using three different approaches.
6816 >>> s.set(mbqi=True)
6817 >>> s.set('MBQI', True)
6818 >>> s.set(':mbqi', True)
6819 """
6820 p = args2params(args, keys, self.ctx)
6821 Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)
6822
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5396
void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p)
Set the given solver using the given parameters.

◆ sexpr()

def sexpr (   self)
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 7237 of file z3py.py.

7237 def sexpr(self):
7238 """Return a formatted string (in Lisp-like format) with all added constraints.
7239 We say the string is in s-expression format.
7240
7241 >>> x = Int('x')
7242 >>> s = Solver()
7243 >>> s.add(x > 0)
7244 >>> s.add(x < 2)
7245 >>> r = s.sexpr()
7246 """
7247 return Z3_solver_to_string(self.ctx.ref(), self.solver)
7248
Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s)
Convert a solver into a string.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

◆ statistics()

def statistics (   self)
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 7175 of file z3py.py.

7175 def statistics(self):
7176 """Return statistics for the last `check()`.
7177
7178 >>> s = SimpleSolver()
7179 >>> x = Int('x')
7180 >>> s.add(x > 0)
7181 >>> s.check()
7182 sat
7183 >>> st = s.statistics()
7184 >>> st.get_key_value('final checks')
7185 1
7186 >>> len(st) > 0
7187 True
7188 >>> st[0] != 0
7189 True
7190 """
7191 return Statistics(Z3_solver_get_statistics(self.ctx.ref(), self.solver), self.ctx)
7192
Z3_stats Z3_API Z3_solver_get_statistics(Z3_context c, Z3_solver s)
Return statistics for the given solver.

◆ to_smt2()

def to_smt2 (   self)
return SMTLIB2 formatted benchmark for solver's assertions

Definition at line 7253 of file z3py.py.

7253 def to_smt2(self):
7254 """return SMTLIB2 formatted benchmark for solver's assertions"""
7255 es = self.assertions()
7256 sz = len(es)
7257 sz1 = sz
7258 if sz1 > 0:
7259 sz1 -= 1
7260 v = (Ast * sz1)()
7261 for i in range(sz1):
7262 v[i] = es[i].as_ast()
7263 if sz > 0:
7264 e = es[sz1].as_ast()
7265 else:
7266 e = BoolVal(True, self.ctx).as_ast()
7268 self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
7269 )
7270
7271
def BoolVal(val, ctx=None)
Definition: z3py.py:1673
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.

◆ trail()

def trail (   self)
Return trail of the solver state after a check() call.

Definition at line 7170 of file z3py.py.

7170 def trail(self):
7171 """Return trail of the solver state after a check() call.
7172 """
7173 return AstVector(Z3_solver_get_trail(self.ctx.ref(), self.solver), self.ctx)
7174
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...

Referenced by Solver.trail_levels().

◆ trail_levels()

def trail_levels (   self)
Return trail and decision levels of the solver state after a check() call.

Definition at line 7162 of file z3py.py.

7162 def trail_levels(self):
7163 """Return trail and decision levels of the solver state after a check() call.
7164 """
7165 trail = self.trail()
7166 levels = (ctypes.c_uint * len(trail))()
7167 Z3_solver_get_levels(self.ctx.ref(), self.solver, trail.vector, len(trail), levels)
7168 return trail, levels
7169
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...

◆ 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 7218 of file z3py.py.

7218 def translate(self, target):
7219 """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
7220
7221 >>> c1 = Context()
7222 >>> c2 = Context()
7223 >>> s1 = Solver(ctx=c1)
7224 >>> s2 = s1.translate(c2)
7225 """
7226 if z3_debug():
7227 _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
7228 solver = Z3_solver_translate(self.ctx.ref(), self.solver, target.ref())
7229 return Solver(solver, target)
7230
def z3_debug()
Definition: z3py.py:64
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.

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().

◆ units()

def units (   self)
Return an AST vector containing all currently inferred units.

Definition at line 7152 of file z3py.py.

7152 def units(self):
7153 """Return an AST vector containing all currently inferred units.
7154 """
7155 return AstVector(Z3_solver_get_units(self.ctx.ref(), self.solver), self.ctx)
7156
Z3_ast_vector Z3_API Z3_solver_get_units(Z3_context c, Z3_solver s)
Return the set of units modulo model conversion.

◆ unsat_core()

def unsat_core (   self)
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 7037 of file z3py.py.

7037 def unsat_core(self):
7038 """Return a subset (as an AST vector) of the assumptions provided to the last check().
7039
7040 These are the assumptions Z3 used in the unsatisfiability proof.
7041 Assumptions are available in Z3. They are used to extract unsatisfiable cores.
7042 They may be also used to "retract" assumptions. Note that, assumptions are not really
7043 "soft constraints", but they can be used to implement them.
7044
7045 >>> p1, p2, p3 = Bools('p1 p2 p3')
7046 >>> x, y = Ints('x y')
7047 >>> s = Solver()
7048 >>> s.add(Implies(p1, x > 0))
7049 >>> s.add(Implies(p2, y > x))
7050 >>> s.add(Implies(p2, y < 1))
7051 >>> s.add(Implies(p3, y > -3))
7052 >>> s.check(p1, p2, p3)
7053 unsat
7054 >>> core = s.unsat_core()
7055 >>> len(core)
7056 2
7057 >>> p1 in core
7058 True
7059 >>> p2 in core
7060 True
7061 >>> p3 in core
7062 False
7063 >>> # "Retracting" p2
7064 >>> s.check(p1, p3)
7065 sat
7066 """
7067 return AstVector(Z3_solver_get_unsat_core(self.ctx.ref(), self.solver), self.ctx)
7068
def Ints(names, ctx=None)
Definition: z3py.py:3223
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...

Field Documentation

◆ backtrack_level

backtrack_level

Definition at line 6796 of file z3py.py.

◆ ctx

ctx

Definition at line 6795 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), FPRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), Probe.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), 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__(), Context.__del__(), AstRef.__del__(), ScopedConstructor.__del__(), ScopedConstructorList.__del__(), ParamsRef.__del__(), ParamDescrsRef.__del__(), 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__(), ArithRef.__div__(), BitVecRef.__div__(), FPRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), Probe.__ge__(), FPRef.__ge__(), SeqRef.__ge__(), QuantifierRef.__getitem__(), ArrayRef.__getitem__(), AstVector.__getitem__(), SeqRef.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), ApplyResult.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), Probe.__gt__(), FPRef.__gt__(), SeqRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), Probe.__le__(), FPRef.__le__(), SeqRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), ApplyResult.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), Probe.__lt__(), FPRef.__lt__(), SeqRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), ArithRef.__mul__(), BitVecRef.__mul__(), FPRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), FPRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), FPRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), FPRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), FPRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), FPRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), ApplyResult.as_expr(), FPNumRef.as_string(), Solver.assert_and_track(), Optimize.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Solver.assertions(), Optimize.assertions(), SeqRef.at(), SeqSortRef.basis(), ReSortRef.basis(), QuantifierRef.body(), BoolSortRef.cast(), Solver.check(), Optimize.check(), UserPropagateBase.conflict(), Solver.consequences(), DatatypeSortRef.constructor(), Goal.convert_model(), AstRef.ctx_ref(), UserPropagateBase.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), Solver.dimacs(), ArraySortRef.domain(), FuncDeclRef.domain(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), FPNumRef.exponent(), FPNumRef.exponent_as_bv(), FPNumRef.exponent_as_long(), Solver.from_file(), Optimize.from_file(), Solver.from_string(), Optimize.from_string(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_documentation(), Fixedpoint.get_ground_sat_answer(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), 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(), FPNumRef.isInf(), FPNumRef.isNaN(), FPNumRef.isNegative(), FPNumRef.isNormal(), FPNumRef.isPositive(), FPNumRef.isSubnormal(), FPNumRef.isZero(), AstMap.keys(), Statistics.keys(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Solver.model(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), QuantifierRef.no_pattern(), Solver.non_units(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), RatNumRef.numerator(), Optimize.objectives(), Solver.param_descrs(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Optimize.pop(), Solver.pop(), Goal.prec(), Solver.proof(), Solver.push(), Optimize.push(), AstVector.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), FuncDeclRef.range(), ArraySortRef.range(), Solver.reason_unknown(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), DatatypeSortRef.recognizer(), Context.ref(), Fixedpoint.register_relation(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), Fixedpoint.set(), Optimize.set(), ParamsRef.set(), Optimize.set_on_model(), Fixedpoint.set_predicate_representation(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), Solver.sexpr(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), FPNumRef.sign(), FPNumRef.sign_as_bv(), FPNumRef.significand(), FPNumRef.significand_as_bv(), FPNumRef.significand_as_long(), ParamDescrsRef.size(), Goal.size(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), QuantifierRef.sort(), ArithRef.sort(), BitVecRef.sort(), ArrayRef.sort(), DatatypeRef.sort(), FiniteDomainRef.sort(), FPRef.sort(), SeqRef.sort(), Solver.statistics(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), Solver.trail(), Solver.trail_levels(), AstVector.translate(), FuncInterp.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), Solver.translate(), Solver.units(), Solver.unsat_core(), Optimize.unsat_core(), Fixedpoint.update_rule(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ cube_vs

cube_vs

Definition at line 7113 of file z3py.py.

Referenced by Solver.cube_vars().

◆ solver

solver