Public Member Functions | |
def | __init__ |
def | __del__ |
def | set |
def | help |
def | param_descrs |
def | assert_exprs |
def | add |
def | append |
def | insert |
def | add_rule |
def | rule |
def | fact |
def | query |
def | push |
def | pop |
def | update_rule |
def | get_answer |
def | get_num_levels |
def | get_cover_delta |
def | add_cover |
def | register_relation |
def | set_predicate_representation |
def | parse_string |
def | parse_file |
def | get_rules |
def | get_assertions |
def | __repr__ |
def | sexpr |
def | to_string |
def | statistics |
def | reason_unknown |
def | declare_var |
def | abstract |
Data Fields | |
ctx | |
fixedpoint | |
vars |
Fixedpoint API provides methods for solving with recursive predicates
def __init__ | ( | self, | |
fixedpoint = None , |
|||
ctx = None |
|||
) |
Definition at line 6094 of file z3py.py.
06094 06095 def __init__(self, fixedpoint=None, ctx=None): 06096 assert fixedpoint == None or ctx != None 06097 self.ctx = _get_ctx(ctx) 06098 self.fixedpoint = None 06099 if fixedpoint == None: 06100 self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref()) 06101 else: 06102 self.fixedpoint = fixedpoint 06103 Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint) 06104 self.vars = []
def __del__ | ( | self | ) |
Definition at line 6105 of file z3py.py.
06105 06106 def __del__(self): 06107 if self.fixedpoint != None: 06108 Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
def __repr__ | ( | self | ) |
def abstract | ( | self, | |
fml, | |||
is_forall = True |
|||
) |
Definition at line 6305 of file z3py.py.
Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), and Fixedpoint.update_rule().
def add | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 6137 of file z3py.py.
06137 06138 def add(self, *args): 06139 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 06140 self.assert_exprs(*args)
def add_cover | ( | self, | |
level, | |||
predicate, | |||
property | |||
) |
Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)
Definition at line 6233 of file z3py.py.
06233 06234 def add_cover(self, level, predicate, property): 06235 """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)""" 06236 Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
def add_rule | ( | self, | |
head, | |||
body = None , |
|||
name = None |
|||
) |
Assert rules defining recursive predicates to the fixedpoint solver. >>> a = Bool('a') >>> b = Bool('b') >>> s = Fixedpoint() >>> s.register_relation(a.decl()) >>> s.register_relation(b.decl()) >>> s.fact(a) >>> s.rule(b, a) >>> s.query(b) sat
Definition at line 6149 of file z3py.py.
Referenced by Fixedpoint.fact(), and Fixedpoint.rule().
06149 06150 def add_rule(self, head, body = None, name = None): 06151 """Assert rules defining recursive predicates to the fixedpoint solver. 06152 >>> a = Bool('a') 06153 >>> b = Bool('b') 06154 >>> s = Fixedpoint() 06155 >>> s.register_relation(a.decl()) 06156 >>> s.register_relation(b.decl()) 06157 >>> s.fact(a) 06158 >>> s.rule(b, a) 06159 >>> s.query(b) 06160 sat 06161 """ 06162 if name == None: 06163 name = "" 06164 name = to_symbol(name, self.ctx) 06165 if body == None: 06166 head = self.abstract(head) 06167 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name) 06168 else: 06169 body = _get_args(body) 06170 f = self.abstract(Implies(And(body),head)) 06171 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def append | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 6141 of file z3py.py.
06141 06142 def append(self, *args): 06143 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 06144 self.assert_exprs(*args)
def assert_exprs | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the fixedpoint solver.
Definition at line 6123 of file z3py.py.
Referenced by Fixedpoint.add(), Fixedpoint.append(), and Fixedpoint.insert().
06123 06124 def assert_exprs(self, *args): 06125 """Assert constraints as background axioms for the fixedpoint solver.""" 06126 args = _get_args(args) 06127 s = BoolSort(self.ctx) 06128 for arg in args: 06129 if isinstance(arg, Goal) or isinstance(arg, AstVector): 06130 for f in arg: 06131 f = self.abstract(f) 06132 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast()) 06133 else: 06134 arg = s.cast(arg) 06135 arg = self.abstract(arg) 06136 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
def declare_var | ( | self, | |
vars | |||
) |
Add variable or several variables. The added variable or variables will be bound in the rules and queries
Definition at line 6296 of file z3py.py.
06296 06297 def declare_var(self, *vars): 06298 """Add variable or several variables. 06299 The added variable or variables will be bound in the rules 06300 and queries 06301 """ 06302 vars = _get_args(vars) 06303 for v in vars: 06304 self.vars += [v]
def fact | ( | self, | |
head, | |||
name = None |
|||
) |
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.
def get_answer | ( | self | ) |
Retrieve answer from last query call.
Definition at line 6219 of file z3py.py.
06219 06220 def get_answer(self): 06221 """Retrieve answer from last query call.""" 06222 r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint) 06223 return _to_expr_ref(r, self.ctx)
def get_assertions | ( | self | ) |
retrieve assertions that have been added to fixedpoint context
Definition at line 6265 of file z3py.py.
06265 06266 def get_assertions(self): 06267 """retrieve assertions that have been added to fixedpoint context""" 06268 return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
def get_cover_delta | ( | self, | |
level, | |||
predicate | |||
) |
Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)
Definition at line 6228 of file z3py.py.
06228 06229 def get_cover_delta(self, level, predicate): 06230 """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)""" 06231 r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast) 06232 return _to_expr_ref(r, self.ctx)
def get_num_levels | ( | self, | |
predicate | |||
) |
Retrieve number of levels used for predicate in PDR engine
Definition at line 6224 of file z3py.py.
06224 06225 def get_num_levels(self, predicate): 06226 """Retrieve number of levels used for predicate in PDR engine""" 06227 return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
def get_rules | ( | self | ) |
retrieve rules that have been added to fixedpoint context
Definition at line 6261 of file z3py.py.
06261 06262 def get_rules(self): 06263 """retrieve rules that have been added to fixedpoint context""" 06264 return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
def help | ( | self | ) |
Display a string describing all available options.
Definition at line 6115 of file z3py.py.
06115 06116 def help(self): 06117 """Display a string describing all available options.""" 06118 print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
def insert | ( | self, | |
args | |||
) |
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.
Definition at line 6145 of file z3py.py.
06145 06146 def insert(self, *args): 06147 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.""" 06148 self.assert_exprs(*args)
def param_descrs | ( | self | ) |
Return the parameter description set.
Definition at line 6119 of file z3py.py.
06119 06120 def param_descrs(self): 06121 """Return the parameter description set.""" 06122 return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
def parse_file | ( | self, | |
f | |||
) |
Parse rules and queries from a file
Definition at line 6257 of file z3py.py.
06257 06258 def parse_file(self, f): 06259 """Parse rules and queries from a file""" 06260 return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
def parse_string | ( | self, | |
s | |||
) |
Parse rules and queries from a string
Definition at line 6253 of file z3py.py.
06253 06254 def parse_string(self, s): 06255 """Parse rules and queries from a string""" 06256 return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
def pop | ( | self | ) |
restore to previously created backtracking point
Definition at line 6206 of file z3py.py.
06206 06207 def pop(self): 06208 """restore to previously created backtracking point""" 06209 Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
def push | ( | self | ) |
create a backtracking point for added rules, facts and assertions
Definition at line 6202 of file z3py.py.
06202 06203 def push(self): 06204 """create a backtracking point for added rules, facts and assertions""" 06205 Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
def query | ( | self, | |
query | |||
) |
Query the fixedpoint engine whether formula is derivable. You can also pass an tuple or list of recursive predicates.
Definition at line 6180 of file z3py.py.
06180 06181 def query(self, *query): 06182 """Query the fixedpoint engine whether formula is derivable. 06183 You can also pass an tuple or list of recursive predicates. 06184 """ 06185 query = _get_args(query) 06186 sz = len(query) 06187 if sz >= 1 and isinstance(query[0], FuncDecl): 06188 _decls = (FuncDecl * sz)() 06189 i = 0 06190 for q in query: 06191 _decls[i] = q.ast 06192 i = i + 1 06193 r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls) 06194 else: 06195 if sz == 1: 06196 query = query[0] 06197 else: 06198 query = And(query) 06199 query = self.abstract(query, False) 06200 r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast()) 06201 return CheckSatResult(r)
def reason_unknown | ( | self | ) |
Return a string describing why the last `query()` returned `unknown`.
Definition at line 6291 of file z3py.py.
06291 06292 def reason_unknown(self): 06293 """Return a string describing why the last `query()` returned `unknown`. 06294 """ 06295 return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
def register_relation | ( | self, | |
relations | |||
) |
Register relation as recursive
Definition at line 6237 of file z3py.py.
06237 06238 def register_relation(self, *relations): 06239 """Register relation as recursive""" 06240 relations = _get_args(relations) 06241 for f in relations: 06242 Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
def rule | ( | self, | |
head, | |||
body = None , |
|||
name = None |
|||
) |
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.
def set | ( | self, | |
args, | |||
keys | |||
) |
Set a configuration option. The method `help()` return a string containing all available options.
Definition at line 6109 of file z3py.py.
06109 06110 def set(self, *args, **keys): 06111 """Set a configuration option. The method `help()` return a string containing all available options. 06112 """ 06113 p = args2params(args, keys, self.ctx) 06114 Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
def set_predicate_representation | ( | self, | |
f, | |||
representations | |||
) |
Control how relation is represented
Definition at line 6243 of file z3py.py.
06243 06244 def set_predicate_representation(self, f, *representations): 06245 """Control how relation is represented""" 06246 representations = _get_args(representations) 06247 representations = [to_symbol(s) for s in representations] 06248 sz = len(representations) 06249 args = (Symbol * sz)() 06250 for i in range(sz): 06251 args[i] = representations[i] 06252 Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
def sexpr | ( | self | ) |
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
Definition at line 6273 of file z3py.py.
Referenced by Fixedpoint.__repr__().
06273 06274 def sexpr(self): 06275 """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. 06276 """ 06277 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
def statistics | ( | self | ) |
Return statistics for the last `query()`.
Definition at line 6286 of file z3py.py.
06286 06287 def statistics(self): 06288 """Return statistics for the last `query()`. 06289 """ 06290 return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
def to_string | ( | self, | |
queries | |||
) |
Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format. Include also queries.
Definition at line 6278 of file z3py.py.
06278 06279 def to_string(self, queries): 06280 """Return a formatted string (in Lisp-like format) with all added constraints. 06281 We say the string is in s-expression format. 06282 Include also queries. 06283 """ 06284 args, len = _to_ast_array(queries) 06285 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
def update_rule | ( | self, | |
head, | |||
body, | |||
name | |||
) |
update rule
Definition at line 6210 of file z3py.py.
06210 06211 def update_rule(self, head, body, name): 06212 """update rule""" 06213 if name == None: 06214 name = "" 06215 name = to_symbol(name, self.ctx) 06216 body = _get_args(body) 06217 f = self.abstract(Implies(And(body),head)) 06218 Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
Definition at line 6094 of file z3py.py.
Referenced by ArithRef::__add__(), BitVecRef::__add__(), BitVecRef::__and__(), FuncDeclRef::__call__(), ArithRef::__div__(), BitVecRef::__div__(), ExprRef::__eq__(), Probe::__eq__(), ArithRef::__ge__(), BitVecRef::__ge__(), Probe::__ge__(), ArrayRef::__getitem__(), ApplyResult::__getitem__(), ArithRef::__gt__(), BitVecRef::__gt__(), Probe::__gt__(), BitVecRef::__invert__(), ArithRef::__le__(), BitVecRef::__le__(), Probe::__le__(), BitVecRef::__lshift__(), ArithRef::__lt__(), BitVecRef::__lt__(), Probe::__lt__(), ArithRef::__mod__(), BitVecRef::__mod__(), ArithRef::__mul__(), BitVecRef::__mul__(), ExprRef::__ne__(), Probe::__ne__(), ArithRef::__neg__(), BitVecRef::__neg__(), BitVecRef::__or__(), ArithRef::__pow__(), ArithRef::__radd__(), BitVecRef::__radd__(), BitVecRef::__rand__(), ArithRef::__rdiv__(), BitVecRef::__rdiv__(), BitVecRef::__rlshift__(), ArithRef::__rmod__(), BitVecRef::__rmod__(), ArithRef::__rmul__(), BitVecRef::__rmul__(), BitVecRef::__ror__(), ArithRef::__rpow__(), BitVecRef::__rrshift__(), BitVecRef::__rshift__(), ArithRef::__rsub__(), BitVecRef::__rsub__(), BitVecRef::__rxor__(), ArithRef::__sub__(), BitVecRef::__sub__(), BitVecRef::__xor__(), DatatypeSortRef::accessor(), Fixedpoint::add_rule(), Tactic::apply(), AlgebraicNumRef::approx(), ExprRef::arg(), ApplyResult::as_expr(), Fixedpoint::assert_exprs(), QuantifierRef::body(), BoolSortRef::cast(), DatatypeSortRef::constructor(), ApplyResult::convert_model(), ExprRef::decl(), RatNumRef::denominator(), FuncDeclRef::domain(), ArraySortRef::domain(), Fixedpoint::get_answer(), Fixedpoint::get_assertions(), Fixedpoint::get_cover_delta(), Fixedpoint::get_rules(), SortRef::kind(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), Fixedpoint::param_descrs(), Tactic::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Fixedpoint::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), Fixedpoint::statistics(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().
Definition at line 6094 of file z3py.py.
Referenced by Fixedpoint.__del__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_num_levels(), Fixedpoint.get_rules(), Fixedpoint.help(), Fixedpoint.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Fixedpoint.push(), Fixedpoint.query(), Fixedpoint.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Fixedpoint.statistics(), Fixedpoint.to_string(), and Fixedpoint.update_rule().
Definition at line 6094 of file z3py.py.
Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().