Z3: Fixedpoint Class Reference

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

Constructor & Destructor Documentation

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

Definition at line 5978 of file z3py.py.

 
     def __init__(self, fixedpoint=None, ctx=None):
         assert fixedpoint == None or ctx != None
         self.ctx    = _get_ctx(ctx)
         self.fixedpoint = None
         if fixedpoint == None:
             self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
         else:
             self.fixedpoint = fixedpoint
         Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
         self.vars = []

Member Function Documentation

def __repr__ ( self )

Return a formatted string with all added rules and constraints.

Definition at line 6153 of file z3py.py.

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

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

Definition at line 6189 of file z3py.py.

 
     def abstract(self, fml, is_forall=True):
         if self.vars == []:
             return fml
         if is_forall:
             return ForAll(self.vars, fml)
         else:
             return Exists(self.vars, fml)

def add	(	self,
		args
	)

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

Definition at line 6021 of file z3py.py.

 
     def add(self, *args):
         """Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
         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 6117 of file z3py.py.

 
     def add_cover(self, level, predicate, property):
         """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
         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 6033 of file z3py.py.

 
     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
         """
         if name == None:
             name = ""
         name = to_symbol(name, self.ctx)
         if body == None:
             head = self.abstract(head)
             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)            
         else:
             body = _get_args(body)
             f    = self.abstract(Implies(And(body),head))
             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 6025 of file z3py.py.

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

def assert_exprs	(	self,
		args
	)

Assert constraints as background axioms for the fixedpoint solver.

Definition at line 6007 of file z3py.py.

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

 
     def assert_exprs(self, *args):
         """Assert constraints as background axioms for the fixedpoint solver."""
         args = _get_args(args)
         s    = BoolSort(self.ctx)
         for arg in args:
             if isinstance(arg, Goal) or isinstance(arg, AstVector):
                 for f in arg:
                     f = self.abstract(f)
                     Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
             else:
                 arg = s.cast(arg)
                 arg = self.abstract(arg)
                 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 6180 of file z3py.py.

 
     def declare_var(self, *vars):
         """Add variable or several variables.
         The added variable or variables will be bound in the rules
         and queries
         """
         vars = _get_args(vars)
         for v in vars:
             self.vars += [v]

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

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

Definition at line 6060 of file z3py.py.

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

def get_answer ( self )

Retrieve answer from last query call.

Definition at line 6103 of file z3py.py.

 
     def get_answer(self):       
         """Retrieve answer from last query call."""
         r = Z3_fixedpoint_get_answer(self.ctx.ref(), self.fixedpoint)
         return _to_expr_ref(r, self.ctx)

def get_assertions ( self )

retrieve assertions that have been added to fixedpoint context

Definition at line 6149 of file z3py.py.

 
     def get_assertions(self):
         """retrieve assertions that have been added to fixedpoint context"""
         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 6112 of file z3py.py.

 
     def get_cover_delta(self, level, predicate):
         """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
         r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
         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 6108 of file z3py.py.

 
     def get_num_levels(self, predicate):
         """Retrieve number of levels used for predicate in PDR engine"""
         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 6145 of file z3py.py.

 
     def get_rules(self):
         """retrieve rules that have been added to fixedpoint context"""
         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 5999 of file z3py.py.

Referenced by Fixedpoint.set().

 
     def help(self):
         """Display a string describing all available options."""
         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 6029 of file z3py.py.

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

def param_descrs ( self )

Return the parameter description set.

Definition at line 6003 of file z3py.py.

 
     def param_descrs(self):
         """Return the parameter description set."""
         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 6141 of file z3py.py.

 
     def parse_file(self, f):
         """Parse rules and queries from a file"""
         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 6137 of file z3py.py.

 
     def parse_string(self, s):
         """Parse rules and queries from a string"""
         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 6090 of file z3py.py.

 
     def pop(self):
         """restore to previously created backtracking point"""
         Z3_fixedpoint_pop(self.ctx.ref(), self.fixedpoint)

def push ( self )

create a backtracking point for added rules, facts and assertions

Definition at line 6086 of file z3py.py.

 
     def push(self):
         """create a backtracking point for added rules, facts and assertions"""
         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 6064 of file z3py.py.

 
     def query(self, *query):
         """Query the fixedpoint engine whether formula is derivable.
            You can also pass an tuple or list of recursive predicates.
         """
         query = _get_args(query)
         sz = len(query)
         if sz >= 1 and isinstance(query[0], FuncDecl):            
             _decls = (FuncDecl * sz)()
             i = 0
             for q in query:
                 _decls[i] = q.ast
                 i = i + 1
             r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
         else:
             if sz == 1:
                 query = query[0]
             else:
                 query = And(query)
             query = self.abstract(query, False)
             r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
         return CheckSatResult(r)

def reason_unknown ( self )

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

Definition at line 6175 of file z3py.py.

 
     def reason_unknown(self):
         """Return a string describing why the last `query()` returned `unknown`.
         """
         return Z3_fixedpoint_get_reason_unknown(self.ctx.ref(), self.fixedpoint)

def register_relation	(	self,
		relations
	)

Register relation as recursive

Definition at line 6121 of file z3py.py.

 
     def register_relation(self, *relations):
         """Register relation as recursive"""
         relations = _get_args(relations)
         for f in relations:
             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.

Definition at line 6056 of file z3py.py.

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

def set	(	self,
		args,
		keys
	)

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

Definition at line 5993 of file z3py.py.

 
     def set(self, *args, **keys):
         """Set a configuration option. The method `help()` return a string containing all available options.        
         """
         p = args2params(args, keys, self.ctx)
         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 6127 of file z3py.py.

 
     def set_predicate_representation(self, f, *representations):
         """Control how relation is represented"""
         representations = _get_args(representations)
         representations = map(to_symbol, representations)
         sz = len(representations)
         args = (Symbol * sz)()
         for i in range(sz):
             args[i] = representations[i]
         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 6157 of file z3py.py.

 
     def sexpr(self):
         """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.        
         """
         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 6170 of file z3py.py.

 
     def statistics(self):
         """Return statistics for the last `query()`.
         """
         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 6162 of file z3py.py.

 
     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.
         """
         args, len = _to_ast_array(queries)
         return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)

def update_rule	(	self,
		head,
		body,
		name
	)

update rule

Definition at line 6094 of file z3py.py.

 
     def update_rule(self, head, body, name):
         """update rule"""
         if name == None:
             name = ""
         name = to_symbol(name, self.ctx)
         body = _get_args(body)
         f    = self.abstract(Implies(And(body),head))
         Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)

Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation