Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Public Member Functions | Data Fields
Fixedpoint Class Reference

Fixedpoint. More...

+ Inheritance diagram for Fixedpoint:

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

Data Fields

 ctx
 
 fixedpoint
 
 vars
 

Detailed Description

Fixedpoint. 

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 6149 of file z3py.py.

Constructor & Destructor Documentation

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

Definition at line 6152 of file z3py.py.

6152 
6153  def __init__(self, fixedpoint=None, ctx=None):
6154  assert fixedpoint == None or ctx != None
6155  self.ctx = _get_ctx(ctx)
6156  self.fixedpoint = None
6157  if fixedpoint == None:
6158  self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
6159  else:
6160  self.fixedpoint = fixedpoint
6161  Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
6162  self.vars = []
Z3_mk_fixedpoint
Z3_fixedpoint Z3_API Z3_mk_fixedpoint(Z3_context c)
Create a new fixedpoint context.
z3py.Fixedpoint.__init__
def __init__
Definition: z3py.py:6152
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.
def __del__ (   self)

Definition at line 6163 of file z3py.py.

6163 
6164  def __del__(self):
6165  if self.fixedpoint != None:
6166  Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
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

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

Definition at line 6327 of file z3py.py.

6327 
6328  def __repr__(self):
6329  """Return a formatted string with all added rules and constraints."""
6330  return self.sexpr()
z3py.Fixedpoint.__repr__
def __repr__
Definition: z3py.py:6327
def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 6363 of file z3py.py.

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

6363 
6364  def abstract(self, fml, is_forall=True):
6365  if self.vars == []:
6366  return fml
6367  if is_forall:
6368  return ForAll(self.vars, fml)
6369  else:
6370  return Exists(self.vars, fml)
6371 
z3py.Exists
def Exists
Definition: z3py.py:1829
z3py.ForAll
def ForAll
Definition: z3py.py:1810
z3py.Fixedpoint.abstract
def abstract
Definition: z3py.py:6363
def add (   self,
  args 
) 
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6195 of file z3py.py.

6195 
6196  def add(self, *args):
6197  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6198  self.assert_exprs(*args)
z3py.Fixedpoint.assert_exprs
def assert_exprs
Definition: z3py.py:6181
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 6291 of file z3py.py.

6291 
6292  def add_cover(self, level, predicate, property):
6293  """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
6294  Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
z3py.Fixedpoint.add_cover
def add_cover
Definition: z3py.py:6291
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...
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 6207 of file z3py.py.

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

6207 
6208  def add_rule(self, head, body = None, name = None):
6209  """Assert rules defining recursive predicates to the fixedpoint solver.
6210  >>> a = Bool('a')
6211  >>> b = Bool('b')
6212  >>> s = Fixedpoint()
6213  >>> s.register_relation(a.decl())
6214  >>> s.register_relation(b.decl())
6215  >>> s.fact(a)
6216  >>> s.rule(b, a)
6217  >>> s.query(b)
6218  sat
6219  """
6220  if name == None:
6221  name = ""
6222  name = to_symbol(name, self.ctx)
6223  if body == None:
6224  head = self.abstract(head)
6225  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
6226  else:
6227  body = _get_args(body)
6228  f = self.abstract(Implies(And(body, self.ctx),head))
6229  Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
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: ...
z3py.Implies
def Implies
Definition: z3py.py:1434
z3py.And
def And
Definition: z3py.py:1489
z3py.Fixedpoint.abstract
def abstract
Definition: z3py.py:6363
z3py.Fixedpoint.add_rule
def add_rule
Definition: z3py.py:6207
z3py.to_symbol
def to_symbol
Definition: z3py.py:94
def append (   self,
  args 
) 
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6199 of file z3py.py.

6199 
6200  def append(self, *args):
6201  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6202  self.assert_exprs(*args)
z3py.Fixedpoint.assert_exprs
def assert_exprs
Definition: z3py.py:6181
def assert_exprs (   self,
  args 
) 
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 6181 of file z3py.py.

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

6181 
6182  def assert_exprs(self, *args):
6183  """Assert constraints as background axioms for the fixedpoint solver."""
6184  args = _get_args(args)
6185  s = BoolSort(self.ctx)
6186  for arg in args:
6187  if isinstance(arg, Goal) or isinstance(arg, AstVector):
6188  for f in arg:
6189  f = self.abstract(f)
6190  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
6191  else:
6192  arg = s.cast(arg)
6193  arg = self.abstract(arg)
6194  Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, arg.as_ast())
z3py.BoolSort
def BoolSort
Definition: z3py.py:1346
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.
z3py.Fixedpoint.abstract
def abstract
Definition: z3py.py:6363
z3py.Fixedpoint.assert_exprs
def assert_exprs
Definition: z3py.py:6181
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 6354 of file z3py.py.

6354 
6355  def declare_var(self, *vars):
6356  """Add variable or several variables.
6357  The added variable or variables will be bound in the rules
6358  and queries
6359  """
6360  vars = _get_args(vars)
6361  for v in vars:
6362  self.vars += [v]
z3py.Fixedpoint.declare_var
def declare_var
Definition: z3py.py:6354
def fact (   self,
  head,
  name = None 
) 
Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6234 of file z3py.py.

6234 
6235  def fact(self, head, name = None):
6236  """Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6237  self.add_rule(head, None, name)
z3py.Fixedpoint.add_rule
def add_rule
Definition: z3py.py:6207
def get_answer (   self) 
Retrieve answer from last query call.

Definition at line 6277 of file z3py.py.

6277 
6278  def get_answer(self):
6279  """Retrieve answer from last query call."""
6280  r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
6281  return _to_expr_ref(r, self.ctx)
z3py.Fixedpoint.get_answer
def get_answer
Definition: z3py.py:6277
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.
def get_assertions (   self) 
retrieve assertions that have been added to fixedpoint context

Definition at line 6323 of file z3py.py.

6323 
6324  def get_assertions(self):
6325  """retrieve assertions that have been added to fixedpoint context"""
6326  return AstVector(Z3_fixedpoint_get_assertions(self.ctx.ref(), self.fixedpoint), self.ctx)
z3py.Fixedpoint.get_assertions
def get_assertions
Definition: z3py.py:6323
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.
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 6286 of file z3py.py.

6286 
6287  def get_cover_delta(self, level, predicate):
6288  """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
6289  r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
6290  return _to_expr_ref(r, self.ctx)
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)
z3py.Fixedpoint.get_cover_delta
def get_cover_delta
Definition: z3py.py:6286
def get_num_levels (   self,
  predicate 
) 
Retrieve number of levels used for predicate in PDR engine

Definition at line 6282 of file z3py.py.

6282 
6283  def get_num_levels(self, predicate):
6284  """Retrieve number of levels used for predicate in PDR engine"""
6285  return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
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. ...
z3py.Fixedpoint.get_num_levels
def get_num_levels
Definition: z3py.py:6282
def get_rules (   self) 
retrieve rules that have been added to fixedpoint context

Definition at line 6319 of file z3py.py.

6319 
6320  def get_rules(self):
6321  """retrieve rules that have been added to fixedpoint context"""
6322  return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
z3py.Fixedpoint.get_rules
def get_rules
Definition: z3py.py:6319
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.
def help (   self) 
Display a string describing all available options.

Definition at line 6173 of file z3py.py.

6173 
6174  def help(self):
6175  """Display a string describing all available options."""
6176  print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
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.
def insert (   self,
  args 
) 
Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr.

Definition at line 6203 of file z3py.py.

6203 
6204  def insert(self, *args):
6205  """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
6206  self.assert_exprs(*args)
z3py.Fixedpoint.assert_exprs
def assert_exprs
Definition: z3py.py:6181
def param_descrs (   self) 
Return the parameter description set.

Definition at line 6177 of file z3py.py.

6177 
6178  def param_descrs(self):
6179  """Return the parameter description set."""
6180  return ParamDescrsRef(Z3_fixedpoint_get_param_descrs(self.ctx.ref(), self.fixedpoint), self.ctx)
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.
z3py.Fixedpoint.param_descrs
def param_descrs
Definition: z3py.py:6177
def parse_file (   self,
  f 
) 
Parse rules and queries from a file

Definition at line 6315 of file z3py.py.

6315 
6316  def parse_file(self, f):
6317  """Parse rules and queries from a file"""
6318  return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
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...
z3py.Fixedpoint.parse_file
def parse_file
Definition: z3py.py:6315
def parse_string (   self,
  s 
) 
Parse rules and queries from a string

Definition at line 6311 of file z3py.py.

6311 
6312  def parse_string(self, s):
6313  """Parse rules and queries from a string"""
6314  return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
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...
z3py.Fixedpoint.parse_string
def parse_string
Definition: z3py.py:6311
def pop (   self) 
restore to previously created backtracking point

Definition at line 6264 of file z3py.py.

6264 
6265  def pop(self):
6266  """restore to previously created backtracking point"""
6267  Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)
Z3_fixedpoint_pop
void Z3_API Z3_fixedpoint_pop(Z3_context c, Z3_fixedpoint d)
Backtrack one backtracking point.
def push (   self) 
create a backtracking point for added rules, facts and assertions

Definition at line 6260 of file z3py.py.

6260 
6261  def push(self):
6262  """create a backtracking point for added rules, facts and assertions"""
6263  Z3_fixedpoint_push(self.ctx.ref(), self.fixedpoint)
Z3_fixedpoint_push
void Z3_API Z3_fixedpoint_push(Z3_context c, Z3_fixedpoint d)
Create a backtracking point.
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 6238 of file z3py.py.

6238 
6239  def query(self, *query):
6240  """Query the fixedpoint engine whether formula is derivable.
6241  You can also pass an tuple or list of recursive predicates.
6242  """
6243  query = _get_args(query)
6244  sz = len(query)
6245  if sz >= 1 and isinstance(query[0], FuncDeclRef):
6246  _decls = (FuncDecl * sz)()
6247  i = 0
6248  for q in query:
6249  _decls[i] = q.ast
6250  i = i + 1
6251  r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
6252  else:
6253  if sz == 1:
6254  query = query[0]
6255  else:
6256  query = And(query, self.ctx)
6257  query = self.abstract(query, False)
6258  r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
6259  return CheckSatResult(r)
z3py.And
def And
Definition: z3py.py:1489
z3py.Fixedpoint.abstract
def abstract
Definition: z3py.py:6363
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.
def reason_unknown (   self) 
Return a string describing why the last `query()` returned `unknown`.

Definition at line 6349 of file z3py.py.

6349 
6350  def reason_unknown(self):
6351  """Return a string describing why the last `query()` returned `unknown`.
6352  """
6353  return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)
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. ...
z3py.Fixedpoint.reason_unknown
def reason_unknown
Definition: z3py.py:6349
def register_relation (   self,
  relations 
) 
Register relation as recursive

Definition at line 6295 of file z3py.py.

6295 
6296  def register_relation(self, *relations):
6297  """Register relation as recursive"""
6298  relations = _get_args(relations)
6299  for f in relations:
6300  Z3_fixedpoint_register_relation(self.ctx.ref(), self.fixedpoint, f.ast)
z3py.Fixedpoint.register_relation
def register_relation
Definition: z3py.py:6295
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...
def rule (   self,
  head,
  body = None,
  name = None 
) 
Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule.

Definition at line 6230 of file z3py.py.

6230 
6231  def rule(self, head, body = None, name = None):
6232  """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
6233  self.add_rule(head, body, name)
z3py.Fixedpoint.add_rule
def add_rule
Definition: z3py.py:6207
def set (   self,
  args,
  keys 
) 
Set a configuration option. The method `help()` return a string containing all available options.

Definition at line 6167 of file z3py.py.

6167 
6168  def set(self, *args, **keys):
6169  """Set a configuration option. The method `help()` return a string containing all available options.
6170  """
6171  p = args2params(args, keys, self.ctx)
6172  Z3_fixedpoint_set_params(self.ctx.ref(), self.fixedpoint, p.params)
z3py.args2params
def args2params
Definition: z3py.py:4527
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.
def set_predicate_representation (   self,
  f,
  representations 
) 
Control how relation is represented

Definition at line 6301 of file z3py.py.

6301 
6302  def set_predicate_representation(self, f, *representations):
6303  """Control how relation is represented"""
6304  representations = _get_args(representations)
6305  representations = [to_symbol(s) for s in representations]
6306  sz = len(representations)
6307  args = (Symbol * sz)()
6308  for i in range(sz):
6309  args[i] = representations[i]
6310  Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
z3py.Fixedpoint.set_predicate_representation
def set_predicate_representation
Definition: z3py.py:6301
z3py.to_symbol
def to_symbol
Definition: z3py.py:94
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.
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 6331 of file z3py.py.

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

6331 
6332  def sexpr(self):
6333  """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
6334  """
6335  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
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.
def statistics (   self) 
Return statistics for the last `query()`.

Definition at line 6344 of file z3py.py.

6344 
6345  def statistics(self):
6346  """Return statistics for the last `query()`.
6347  """
6348  return Statistics(Z3_fixedpoint_get_statistics(self.ctx.ref(), self.fixedpoint), self.ctx)
z3py.Fixedpoint.statistics
def statistics
Definition: z3py.py:6344
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.
z3py.Statistics
Statistics.
Definition: z3py.py:5604
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 6336 of file z3py.py.

6336 
6337  def to_string(self, queries):
6338  """Return a formatted string (in Lisp-like format) with all added constraints.
6339  We say the string is in s-expression format.
6340  Include also queries.
6341  """
6342  args, len = _to_ast_array(queries)
6343  return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
z3py.Fixedpoint.to_string
def to_string
Definition: z3py.py:6336
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.
def update_rule (   self,
  head,
  body,
  name 
) 
update rule

Definition at line 6268 of file z3py.py.

6268 
6269  def update_rule(self, head, body, name):
6270  """update rule"""
6271  if name == None:
6272  name = ""
6273  name = to_symbol(name, self.ctx)
6274  body = _get_args(body)
6275  f = self.abstract(Implies(And(body, self.ctx),head))
6276  Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
z3py.Implies
def Implies
Definition: z3py.py:1434
z3py.And
def And
Definition: z3py.py:1489
z3py.Fixedpoint.abstract
def abstract
Definition: z3py.py:6363
z3py.Fixedpoint.update_rule
def update_rule
Definition: z3py.py:6268
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. ...
z3py.to_symbol
def to_symbol
Definition: z3py.py:94

Field Documentation

ctx

Definition at line 6154 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), Optimize.model(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), and Fixedpoint.update_rule().

fixedpoint

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

vars

Definition at line 6161 of file z3py.py.

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

Generated on Fri Apr 12 2019 11:38:55 for Z3 by   doxygen 1.8.5