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

    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 = []

def __del__

(

self

)

Definition at line 6163 of file z3py.py.

    def __del__(self):
        if self.fixedpoint != None:
            Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)

---

Member Function Documentation

def __repr__

(

self

)

Return a formatted string with all added rules and constraints.

Definition at line 6327 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 6363 of file z3py.py.

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

    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 6195 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 6291 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 6207 of file z3py.py.

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

06207 
06208     def add_rule(self, head, body = None, name = None):
06209         """Assert rules defining recursive predicates to the fixedpoint solver.
06210         >>> a = Bool('a')
06211         >>> b = Bool('b')
06212         >>> s = Fixedpoint()
06213         >>> s.register_relation(a.decl())
06214         >>> s.register_relation(b.decl())
06215         >>> s.fact(a)
06216         >>> s.rule(b, a)
06217         >>> s.query(b)
06218         sat
06219         """
06220         if name == None:
06221             name = ""
06222         name = to_symbol(name, self.ctx)
06223         if body == None:
06224             head = self.abstract(head)
06225             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)            
06226         else:
06227             body = _get_args(body)
06228             f    = self.abstract(Implies(And(body, self.ctx),head))
06229             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 6199 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 6181 of file z3py.py.

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

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

06354 
06355     def declare_var(self, *vars):
06356         """Add variable or several variables.
06357         The added variable or variables will be bound in the rules
06358         and queries
06359         """
06360         vars = _get_args(vars)
06361         for v in vars:
06362             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 6234 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 6277 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 6323 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 6286 of file z3py.py.

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

06173 
06174     def help(self):
06175         """Display a string describing all available options."""
06176         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 6203 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 6177 of file z3py.py.

06177 
06178     def param_descrs(self):
06179         """Return the parameter description set."""
06180         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 6315 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 6311 of file z3py.py.

06311 
06312     def parse_string(self, s):
06313         """Parse rules and queries from a string"""
06314         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 6264 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 6260 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 6238 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], FuncDeclRef):            
            _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, self.ctx)
            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 6349 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 6295 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 6230 of file z3py.py.

06230 
06231     def rule(self, head, body = None, name = None):
06232         """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
06233         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 6167 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 6301 of file z3py.py.

    def set_predicate_representation(self, f, *representations):
        """Control how relation is represented"""
        representations = _get_args(representations)
        representations = [to_symbol(s) for s in 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 6331 of file z3py.py.

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

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

06336 
06337     def to_string(self, queries):
06338         """Return a formatted string (in Lisp-like format) with all added constraints.
06339            We say the string is in s-expression format.
06340            Include also queries.
06341         """
06342         args, len = _to_ast_array(queries)
06343         return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
    

def update_rule	(		self,
			head,
			body,
			name
	)

update rule

Definition at line 6268 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, self.ctx),head))
        Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)

---

Field Documentation

ctx

Definition at line 6152 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(), Optimize::add_soft(), 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(), ArrayRef::mk_default(), Optimize::model(), SortRef::name(), FuncDeclRef::name(), QuantifierRef::no_pattern(), RatNumRef::numerator(), Fixedpoint::param_descrs(), Optimize::param_descrs(), Tactic::param_descrs(), Fixedpoint::parse_file(), Fixedpoint::parse_string(), QuantifierRef::pattern(), Fixedpoint::query(), FuncDeclRef::range(), ArraySortRef::range(), DatatypeSortRef::recognizer(), Fixedpoint::set(), Optimize::set(), Tactic::solver(), ExprRef::sort(), BoolRef::sort(), QuantifierRef::sort(), ArithRef::sort(), BitVecRef::sort(), ArrayRef::sort(), DatatypeRef::sort(), Fixedpoint::statistics(), Optimize::statistics(), Fixedpoint::update_rule(), QuantifierRef::var_name(), and QuantifierRef::var_sort().

fixedpoint

Definition at line 6152 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 6152 of file z3py.py.

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