Z3 |

Public Member Functions | Data Fields
Fixedpoint Class Reference

Fixedpoint. More...

Inheritance diagram for Fixedpoint:

## Public Member Functions
def | __init__ (self, fixedpoint=None, ctx=None)
def | __deepcopy__ (self, memo={})
def | __del__ (self)
def | set (self, *args, **keys)
def | help (self)
def | param_descrs (self)
def | assert_exprs (self, *args)
def | add (self, *args)
def | __iadd__ (self, fml)
def | append (self, *args)
def | insert (self, *args)
def | add_rule (self, head, body=None, name=None)
def | rule (self, head, body=None, name=None)
def | fact (self, head, name=None)
def | query (self, *query)
def | query_from_lvl (self, lvl, *query)
def | update_rule (self, head, body, name)
def | get_answer (self)
def | get_ground_sat_answer (self)
def | get_rules_along_trace (self)
def | get_rule_names_along_trace (self)
def | get_num_levels (self, predicate)
def | get_cover_delta (self, level, predicate)
def | add_cover (self, level, predicate, property)
def | register_relation (self, *relations)
def | set_predicate_representation (self, f, *representations)
def | parse_string (self, s)
def | parse_file (self, f)
def | get_rules (self)
def | get_assertions (self)
def | __repr__ (self)
def | sexpr (self)
def | to_string (self, queries)
def | statistics (self)
def | reason_unknown (self)
def | declare_var (self, *vars)
def | abstract (self, fml, is_forall=True)
Public Member Functions inherited from Z3PPObject
def | use_pp (self)

## Data Fields
| ctx
| fixedpoint
| vars

## Detailed Description

Fixedpoint.

    Fixedpoint API provides methods for solving with recursive predicates

Definition at line 7312 of file z3py.py.

## Constructor & Destructor Documentation

## ◆ __init__()

def __init__ | ( |  | self,
|  |  | fixedpoint = `None`,
|  |  | ctx = `None`
| ) |  |

Definition at line 7315 of file z3py.py.

7315 def __init__(self, fixedpoint=None, ctx=None):
7316 assert fixedpoint is None or ctx is not None
7317 self.ctx = _get_ctx(ctx)
7318 self.fixedpoint = None
7319 if fixedpoint is None:
7320 self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
7321 else:
7322 self.fixedpoint = fixedpoint
7323 Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
7324 self.vars = []
7325
Z3_fixedpoint_inc_ref
void Z3_API Z3_fixedpoint_inc_ref(Z3_context c, Z3_fixedpoint d)
Increment the reference counter of the given fixedpoint context.
Z3_mk_fixedpoint
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.

## ◆ __del__()

def __del__ | ( |  | self | ) |

Definition at line 7329 of file z3py.py.

7329 def __del__(self):
7330 if self.fixedpoint is not None and self.ctx.ref() is not None:
7331 Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
7332
Z3_fixedpoint_dec_ref
void Z3_API Z3_fixedpoint_dec_ref(Z3_context c, Z3_fixedpoint d)
Decrement the reference counter of the given fixedpoint context.

## Member Function Documentation

## ◆ __deepcopy__()

def __deepcopy__ | ( |  | self,
|  |  | memo = `{}`
| ) |  |

Definition at line 7326 of file z3py.py.

7326 def __deepcopy__(self, memo={}):
7327 return FixedPoint(self.fixedpoint, self.ctx)
7328

## ◆ __iadd__()

def __iadd__ | ( |  | self,
|  |  | fml
| ) |  |

Definition at line 7365 of file z3py.py.

7365 def __iadd__(self, fml):
7366 self.add(fml)
7367 return self
7368

## ◆ __repr__()

def __repr__ | ( |  | self | ) |

    Return a formatted string with all added rules and constraints.

Definition at line 7526 of file z3py.py.

7526 def __repr__(self):
7527 """Return a formatted string with all added rules and constraints."""
7528 return self.sexpr()
7529

## ◆ abstract()

def abstract | ( |  | self,
|  |  | fml,
|  |  | is_forall = `True`
| ) |  |

Definition at line 7563 of file z3py.py.

7563 def abstract(self, fml, is_forall=True):
7564 if self.vars == []:
7565 return fml
7566 if is_forall:
7567 return ForAll(self.vars, fml)
7568 else:
7569 return Exists(self.vars, fml)
7570
7571
z3py.ForAll
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2187
z3py.Exists
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[])
Definition: z3py.py:2205

Referenced by Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), and Fixedpoint.update_rule().

## ◆ add()

def add | ( |  | self,
|  | * | args
| ) |  |

    Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7361 of file z3py.py.

7361 def add(self, *args):
7362 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7363 self.assert_exprs(*args)
7364

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

## ◆ add_cover()

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

7488 def add_cover(self, level, predicate, property):
7489 """Add property to predicate for the level'th unfolding.
7490 -1 is treated as infinity (infinity)
7491 """
7492 Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
7493
Z3_fixedpoint_add_cover
void Z3_API Z3_fixedpoint_add_cover(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred, Z3_ast property)
Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forw...

## ◆ add_rule()

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

7377 def add_rule(self, head, body=None, name=None):
7378 """Assert rules defining recursive predicates to the fixedpoint solver.
7379 >>> a = Bool('a')
7380 >>> b = Bool('b')
7381 >>> s = Fixedpoint()
7382 >>> s.register_relation(a.decl())
7383 >>> s.register_relation(b.decl())
7384 >>> s.fact(a)
7385 >>> s.rule(b, a)
7386 >>> s.query(b)
7387 sat
7388 """
7389 if name is None:
7390 name = ""
7391 name = to_symbol(name, self.ctx)
7392 if body is None:
7393 head = self.abstract(head)
7394 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
7395 else:
7396 body = _get_args(body)
7397 f = self.abstract(Implies(And(body, self.ctx), head))
7398 Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7399
z3py.Implies
def Implies(a, b, ctx=None)
Definition: z3py.py:1749
z3py.Bool
def Bool(name, ctx=None)
Definition: z3py.py:1692
z3py.to_symbol
def to_symbol(s, ctx=None)
Definition: z3py.py:129
z3py.And
def And(*args)
Definition: z3py.py:1813
Z3_fixedpoint_add_rule
void Z3_API Z3_fixedpoint_add_rule(Z3_context c, Z3_fixedpoint d, Z3_ast rule, Z3_symbol name)
Add a universal Horn clause as a named rule. The horn_rule should be of the form:

Referenced by Fixedpoint.fact(), and Fixedpoint.rule().

## ◆ append()

def append | ( |  | self,
|  | * | args
| ) |  |

    Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7369 of file z3py.py.

7369 def append(self, *args):
7370 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7371 self.assert_exprs(*args)
7372

## ◆ assert_exprs()

def assert_exprs | ( |  | self,
|  | * | args
| ) |  |

    Assert constraints as background axioms for the fixedpoint solver.

Definition at line 7347 of file z3py.py.

7347 def assert_exprs(self, *args):
7348 """Assert constraints as background axioms for the fixedpoint solver."""
7349 args = _get_args(args)
7350 s = BoolSort(self.ctx)
7351 for arg in args:
7352 if isinstance(arg, Goal) or isinstance(arg, AstVector):
7353 for f in arg:
7354 f = self.abstract(f)
7355 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
7356 else:
7357 arg = s.cast(arg)
7358 arg = self.abstract(arg)
7359 Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
7360
z3py.BoolSort
def BoolSort(ctx=None)
Definition: z3py.py:1655
Z3_fixedpoint_assert
void Z3_API Z3_fixedpoint_assert(Z3_context c, Z3_fixedpoint d, Z3_ast axiom)
Assert a constraint to the fixedpoint context.

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

## ◆ declare_var()

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

7554 def declare_var(self, *vars):
7555 """Add variable or several variables.
7556 The added variable or variables will be bound in the rules
7557 and queries
7558 """
7559 vars = _get_args(vars)
7560 for v in vars:
7561 self.vars += [v]
7562

## ◆ fact()

def fact | ( |  | self,
|  |  | head,
|  |  | name = `None`
| ) |  |

    Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7404 of file z3py.py.

7404 def fact(self, head, name=None):
7405 """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7406 self.add_rule(head, None, name)
7407

## ◆ get_answer()

def get_answer | ( |  | self | ) |

    Retrieve answer from last query call.

Definition at line 7455 of file z3py.py.

7455 def get_answer(self):
7456 """Retrieve answer from last query call."""
7457 r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
7458 return _to_expr_ref(r, self.ctx)
7459
Z3_fixedpoint_get_answer
Z3_ast Z3_API Z3_fixedpoint_get_answer(Z3_context c, Z3_fixedpoint d)
Retrieve a formula that encodes satisfying answers to the query.

## ◆ get_assertions()

def get_assertions | ( |  | self | ) |

    retrieve assertions that have been added to fixedpoint context

Definition at line 7522 of file z3py.py.

7522 def get_assertions(self):
7523 """retrieve assertions that have been added to fixedpoint context"""
7524 return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
7525
Z3_fixedpoint_get_assertions
Z3_ast_vector Z3_API Z3_fixedpoint_get_assertions(Z3_context c, Z3_fixedpoint f)
Retrieve set of background assertions from fixedpoint context.

## ◆ get_cover_delta()

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

7481 def get_cover_delta(self, level, predicate):
7482 """Retrieve properties known about predicate for the level'th unfolding.
7483 -1 is treated as the limit (infinity)
7484 """
7485 r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
7486 return _to_expr_ref(r, self.ctx)
7487
Z3_fixedpoint_get_cover_delta
Z3_ast Z3_API Z3_fixedpoint_get_cover_delta(Z3_context c, Z3_fixedpoint d, int level, Z3_func_decl pred)

## ◆ get_ground_sat_answer()

def get_ground_sat_answer | ( |  | self | ) |

    Retrieve a ground cex from last query call.

Definition at line 7460 of file z3py.py.

7460 def get_ground_sat_answer(self):
7461 """Retrieve a ground cex from last query call."""
7462 r = Z3_fixedpoint_get_ground_sat_answer(self.ctx.ref(), self.fixedpoint)
7463 return _to_expr_ref(r, self.ctx)
7464

## ◆ get_num_levels()

def get_num_levels | ( |  | self,
|  |  | predicate
| ) |  |

    Retrieve number of levels used for predicate in PDR engine

Definition at line 7477 of file z3py.py.

7477 def get_num_levels(self, predicate):
7478 """Retrieve number of levels used for predicate in PDR engine"""
7479 return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
7480
Z3_fixedpoint_get_num_levels
unsigned Z3_API Z3_fixedpoint_get_num_levels(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred)
Query the PDR engine for the maximal levels properties are known about predicate.

## ◆ get_rule_names_along_trace()

def get_rule_names_along_trace | ( |  | self | ) |

    retrieve rule names along the counterexample trace

Definition at line 7469 of file z3py.py.

7469 def get_rule_names_along_trace(self):
7470 """retrieve rule names along the counterexample trace"""
7471 # this is a hack as I don't know how to return a list of symbols from C++;
7472 # obtain names as a single string separated by semicolons
7473 names = _symbol2py(self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
7474 # split into individual names
7475 return names.split(";")
7476

## ◆ get_rules()

def get_rules | ( |  | self | ) |

    retrieve rules that have been added to fixedpoint context

Definition at line 7518 of file z3py.py.

7518 def get_rules(self):
7519 """retrieve rules that have been added to fixedpoint context"""
7520 return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
7521
Z3_fixedpoint_get_rules
Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(Z3_context c, Z3_fixedpoint f)
Retrieve set of rules from fixedpoint context.

## ◆ get_rules_along_trace()

def get_rules_along_trace | ( |  | self | ) |

    retrieve rules along the counterexample trace

Definition at line 7465 of file z3py.py.

7465 def get_rules_along_trace(self):
7466 """retrieve rules along the counterexample trace"""
7467 return AstVector(Z3_fixedpoint_get_rules_along_trace(self.ctx.ref(), self.fixedpoint), self.ctx)
7468

## ◆ help()

def help | ( |  | self | ) |

    Display a string describing all available options.

Definition at line 7339 of file z3py.py.

7339 def help(self):
7340 """Display a string describing all available options."""
7341 print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
7342
Z3_fixedpoint_get_help
Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f)
Return a string describing all fixedpoint available parameters.

## ◆ insert()

def insert | ( |  | self,
|  | * | args
| ) |  |

    Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 7373 of file z3py.py.

7373 def insert(self, *args):
7374 """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
7375 self.assert_exprs(*args)
7376

## ◆ param_descrs()

def param_descrs | ( |  | self | ) |

    Return the parameter description set.

Definition at line 7343 of file z3py.py.

7343 def param_descrs(self):
7344 """Return the parameter description set."""
7345 return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
7346
Z3_fixedpoint_get_param_descrs
Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f)
Return the parameter description set for the given fixedpoint object.

## ◆ parse_file()

def parse_file | ( |  | self,
|  |  | f
| ) |  |

    Parse rules and queries from a file

Definition at line 7514 of file z3py.py.

7514 def parse_file(self, f):
7515 """Parse rules and queries from a file"""
7516 return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
7517
Z3_fixedpoint_from_file
Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context....

## ◆ parse_string()

def parse_string | ( |  | self,
|  |  | s
| ) |  |

    Parse rules and queries from a string

Definition at line 7510 of file z3py.py.

7510 def parse_string(self, s):
7511 """Parse rules and queries from a string"""
7512 return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
7513
Z3_fixedpoint_from_string
Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, Z3_fixedpoint f, Z3_string s)
Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context....

## ◆ query()

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

7408 def query(self, *query):
7409 """Query the fixedpoint engine whether formula is derivable.
7410 You can also pass an tuple or list of recursive predicates.
7411 """
7412 query = _get_args(query)
7413 sz = len(query)
7414 if sz >= 1 and isinstance(query[0], FuncDeclRef):
7415 _decls = (FuncDecl * sz)()
7416 i = 0
7417 for q in query:
7418 _decls[i] = q.ast
7419 i = i + 1
7420 r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
7421 else:
7422 if sz == 1:
7423 query = query[0]
7424 else:
7425 query = And(query, self.ctx)
7426 query = self.abstract(query, False)
7427 r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
7428 return CheckSatResult(r)
7429
Z3_fixedpoint_query
Z3_lbool Z3_API Z3_fixedpoint_query(Z3_context c, Z3_fixedpoint d, Z3_ast query)
Pose a query against the asserted rules.
Z3_fixedpoint_query_relations
Z3_lbool Z3_API Z3_fixedpoint_query_relations(Z3_context c, Z3_fixedpoint d, unsigned num_relations, Z3_func_decl const relations[])
Pose multiple queries against the asserted rules.

## ◆ query_from_lvl()

def query_from_lvl | ( |  | self,
|  |  | lvl,
|  | * | query
| ) |  |

    Query the fixedpoint engine whether formula is derivable starting at the given query level.

Definition at line 7430 of file z3py.py.

7430 def query_from_lvl(self, lvl, *query):
7431 """Query the fixedpoint engine whether formula is derivable starting at the given query level.
7432 """
7433 query = _get_args(query)
7434 sz = len(query)
7435 if sz >= 1 and isinstance(query[0], FuncDecl):
7436 _z3_assert(False, "unsupported")
7437 else:
7438 if sz == 1:
7439 query = query[0]
7440 else:
7441 query = And(query)
7442 query = self.abstract(query, False)
7443 r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
7444 return CheckSatResult(r)
7445

## ◆ reason_unknown()

def reason_unknown | ( |  | self | ) |

    Return a string describing why the last `query()` returned `unknown`.

Definition at line 7549 of file z3py.py.

7549 def reason_unknown(self):
7550 """Return a string describing why the last `query()` returned `unknown`.
7551 """
7552 return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
7553
Z3_fixedpoint_get_reason_unknown
Z3_string Z3_API Z3_fixedpoint_get_reason_unknown(Z3_context c, Z3_fixedpoint d)
Retrieve a string that describes the last status returned by Z3_fixedpoint_query.

## ◆ register_relation()

def register_relation | ( |  | self,
|  | * | relations
| ) |  |

    Register relation as recursive

Definition at line 7494 of file z3py.py.

7494 def register_relation(self, *relations):
7495 """Register relation as recursive"""
7496 relations = _get_args(relations)
7497 for f in relations:
7498 Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
7499
Z3_fixedpoint_register_relation
void Z3_API Z3_fixedpoint_register_relation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f)
Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics...

## ◆ rule()

def rule | ( |  | self,
|  |  | head,
|  |  | body = `None`,
|  |  | name = `None`
| ) |  |

    Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 7400 of file z3py.py.

7400 def rule(self, head, body=None, name=None):
7401 """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
7402 self.add_rule(head, body, name)
7403

## ◆ set()

def set | ( |  | self,
|  | * | args,
|  | ** | keys
| ) |  |

    Set a configuration option. The method `help()` return a string containing all available options.

Definition at line 7333 of file z3py.py.

7333 def set(self, *args, **keys):
7334 """Set a configuration option. The method `help()` return a string containing all available options.
7335 """
7336 p = args2params(args, keys, self.ctx)
7337 Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
7338
z3py.args2params
def args2params(arguments, keywords, ctx=None)
Definition: z3py.py:5396
Z3_fixedpoint_set_params
void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p)
Set parameters on fixedpoint context.

## ◆ set_predicate_representation()

def set_predicate_representation | ( |  | self,
|  |  | f,
|  | * | representations
| ) |  |

    Control how relation is represented

Definition at line 7500 of file z3py.py.

7500 def set_predicate_representation(self, f, *representations):
7501 """Control how relation is represented"""
7502 representations = _get_args(representations)
7503 representations = [to_symbol(s) for s in representations]
7504 sz = len(representations)
7505 args = (Symbol * sz)()
7506 for i in range(sz):
7507 args[i] = representations[i]
7508 Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
7509
z3::range
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:3725
Z3_fixedpoint_set_predicate_representation
void Z3_API Z3_fixedpoint_set_predicate_representation(Z3_context c, Z3_fixedpoint d, Z3_func_decl f, unsigned num_relations, Z3_symbol const relation_kinds[])
Configure the predicate representation.

## ◆ 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.

Definition at line 7530 of file z3py.py.

7530 def sexpr(self):
7531 """Return a formatted string (in Lisp-like format) with all added constraints.
7532 We say the string is in s-expression format.
7533 """
7534 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
7535
Z3_fixedpoint_to_string
Z3_string Z3_API Z3_fixedpoint_to_string(Z3_context c, Z3_fixedpoint f, unsigned num_queries, Z3_ast queries[])
Print the current rules and background axioms as a string.

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

## ◆ statistics()

def statistics | ( |  | self | ) |

    Return statistics for the last `query()`.

Definition at line 7544 of file z3py.py.

7544 def statistics(self):
7545 """Return statistics for the last `query()`.
7546 """
7547 return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
7548
Z3_fixedpoint_get_statistics
Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c, Z3_fixedpoint d)
Retrieve statistics information from the last call to Z3_fixedpoint_query.

## ◆ to_string()

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

7536 def to_string(self, queries):
7537 """Return a formatted string (in Lisp-like format) with all added constraints.
7538 We say the string is in s-expression format.
7539 Include also queries.
7540 """
7541 args, len = _to_ast_array(queries)
7542 return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
7543

## ◆ update_rule()

def update_rule | ( |  | self,
|  |  | head,
|  |  | body,
|  |  | name
| ) |  |

    update rule

Definition at line 7446 of file z3py.py.

7446 def update_rule(self, head, body, name):
7447 """update rule"""
7448 if name is None:
7449 name = ""
7450 name = to_symbol(name, self.ctx)
7451 body = _get_args(body)
7452 f = self.abstract(Implies(And(body, self.ctx), head))
7453 Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
7454
Z3_fixedpoint_update_rule
void Z3_API Z3_fixedpoint_update_rule(Z3_context c, Z3_fixedpoint d, Z3_ast a, Z3_symbol name)
Update a named rule. A rule with the same name must have been previously created.

## Field Documentation

## ◆ ctx

ctx

Definition at line 7317 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().

## ◆ fixedpoint

fixedpoint

Definition at line 7318 of file z3py.py.

Referenced by Fixedpoint.__deepcopy__(), Fixedpoint.__del__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Fixedpoint.assert_exprs(), 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(), Fixedpoint.help(), Fixedpoint.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Fixedpoint.statistics(), Fixedpoint.to_string(), and Fixedpoint.update_rule().

## ◆ vars

vars

Definition at line 7324 of file z3py.py.

Referenced by Fixedpoint.abstract(), and Fixedpoint.declare_var().