Fixedpoint. More...

Inheritance diagram for Fixedpoint:

Public Member Functions
	__init__ (self, fixedpoint=None, ctx=None)

	__deepcopy__ (self, memo={})

	__del__ (self)

	set (self, args, *keys)

	help (self)

	param_descrs (self)

	assert_exprs (self, *args)

	add (self, *args)

	__iadd__ (self, fml)

	append (self, *args)

	insert (self, *args)

	add_rule (self, head, body=None, name=None)

	rule (self, head, body=None, name=None)

	fact (self, head, name=None)

	query (self, *query)

	query_from_lvl (self, lvl, *query)

	update_rule (self, head, body, name)

	get_answer (self)

	get_ground_sat_answer (self)

	get_rules_along_trace (self)

	get_rule_names_along_trace (self)

	get_num_levels (self, predicate)

	get_cover_delta (self, level, predicate)

	add_cover (self, level, predicate, property)

	register_relation (self, *relations)

	set_predicate_representation (self, f, *representations)

	parse_string (self, s)

	parse_file (self, f)

	get_rules (self)

	get_assertions (self)

	__repr__ (self)

	sexpr (self)

	to_string (self, queries)

	statistics (self)

	reason_unknown (self)

	declare_var (self, *vars)

	abstract (self, fml, is_forall=True)

Public Member Functions inherited from Z3PPObject
	use_pp (self)

Data Fields
	ctx

	fixedpoint

	vars

Additional Inherited Members
Protected Member Functions inherited from Z3PPObject
	_repr_html_ (self)

Detailed Description

Fixedpoint.

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 7696 of file z3py.py.

Constructor & Destructor Documentation

◆ init()

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

Definition at line 7699 of file z3py.py.

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

◆ del()

__del__ ( self )

Definition at line 7713 of file z3py.py.

    def __del__(self):
        if self.fixedpoint is not None and self.ctx.ref() is not None and Z3_fixedpoint_dec_ref is not None:
            Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint)
 

Member Function Documentation

◆ deepcopy()

__deepcopy__	(	self,
		memo = `{}`
	)

Definition at line 7710 of file z3py.py.

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

◆ iadd()

__iadd__	(	self,
		fml
	)

Definition at line 7749 of file z3py.py.

    def __iadd__(self, fml):
        self.add(fml)
        return self
 

◆ repr()

__repr__ ( self )

Return a formatted string with all added rules and constraints.

Definition at line 7910 of file z3py.py.

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

◆ abstract()

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

Definition at line 7947 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)
 
 

◆ add()

add	(		self,
		*	args
	)

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

Definition at line 7745 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)
 

Referenced by Solver.__iadd__().

◆ add_cover()

add_cover	(	self,
		level,
		predicate,
		property
	)

Add property to predicate for the level'th unfolding.
-1 is treated as infinity (infinity)

Definition at line 7872 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)
 

◆ add_rule()

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 7761 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 is None:
            name = ""
        name = to_symbol(name, self.ctx)
        if body is 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, self.ctx), head))
            Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
 

◆ append()

append	(		self,
		*	args
	)

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

Definition at line 7753 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)
 

◆ assert_exprs()

assert_exprs	(		self,
		*	args
	)

Assert constraints as background axioms for the fixedpoint solver.

Definition at line 7731 of file z3py.py.

    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())
 

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

◆ declare_var()

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 7938 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]
 

◆ fact()

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

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

Definition at line 7788 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)
 

◆ get_answer()

get_answer ( self )

Retrieve answer from last query call.

Definition at line 7839 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)
 

◆ get_assertions()

get_assertions ( self )

retrieve assertions that have been added to fixedpoint context

Definition at line 7906 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)
 

◆ get_cover_delta()

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 7865 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)
 

◆ get_ground_sat_answer()

get_ground_sat_answer ( self )

Retrieve a ground cex from last query call.

Definition at line 7844 of file z3py.py.

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

◆ get_num_levels()

get_num_levels	(	self,
		predicate
	)

Retrieve number of levels used for predicate in PDR engine

Definition at line 7861 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)
 

◆ get_rule_names_along_trace()

get_rule_names_along_trace ( self )

retrieve rule names along the counterexample trace

Definition at line 7853 of file z3py.py.

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

◆ get_rules()

get_rules ( self )

retrieve rules that have been added to fixedpoint context

Definition at line 7902 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)
 

◆ get_rules_along_trace()

get_rules_along_trace ( self )

retrieve rules along the counterexample trace

Definition at line 7849 of file z3py.py.

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

◆ help()

help ( self )

Display a string describing all available options.

Definition at line 7723 of file z3py.py.

    def help(self):
        """Display a string describing all available options."""
        print(Z3_fixedpoint_get_help(self.ctx.ref(), self.fixedpoint))
 

◆ insert()

insert	(		self,
		*	args
	)

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

Definition at line 7757 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)
 

◆ param_descrs()

param_descrs ( self )

Return the parameter description set.

Definition at line 7727 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)
 

◆ parse_file()

parse_file	(	self,
		f
	)

Parse rules and queries from a file

Definition at line 7898 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)
 

◆ parse_string()

parse_string	(	self,
		s
	)

Parse rules and queries from a string

Definition at line 7894 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)
 

◆ query()

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 7792 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)
 

◆ query_from_lvl()

query_from_lvl	(		self,
			lvl,
		*	query
	)

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

Definition at line 7814 of file z3py.py.

    def query_from_lvl(self, lvl, *query):
        """Query the fixedpoint engine whether formula is derivable starting at the given query level.
        """
        query = _get_args(query)
        sz = len(query)
        if sz >= 1 and isinstance(query[0], FuncDecl):
            _z3_assert(False, "unsupported")
        else:
            if sz == 1:
                query = query[0]
            else:
                query = And(query)
            query = self.abstract(query, False)
            r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
        return CheckSatResult(r)
 

◆ reason_unknown()

reason_unknown ( self )

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

Definition at line 7933 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)
 

◆ register_relation()

register_relation	(		self,
		*	relations
	)

Register relation as recursive

Definition at line 7878 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)
 

◆ rule()

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

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

Definition at line 7784 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)
 

◆ set()

set	(		self,
		*	args,
		**	keys
	)

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

Definition at line 7717 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)
 

◆ set_predicate_representation()

set_predicate_representation	(		self,
			f,
		*	representations
	)

Control how relation is represented

Definition at line 7884 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)
 

◆ sexpr()

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 7914 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)())
 

◆ statistics()

statistics ( self )

Return statistics for the last `query()`.

Definition at line 7928 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)
 

◆ to_string()

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 7920 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)
 

◆ update_rule()

update_rule	(	self,
		head,
		body,
		name
	)

update rule

Definition at line 7830 of file z3py.py.

    def update_rule(self, head, body, name):
        """update rule"""
        if name is 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

ctx

Definition at line 7701 of file z3py.py.

Referenced by ArithRef.__add__(), BitVecRef.__add__(), BitVecRef.__and__(), FuncDeclRef.__call__(), AstMap.__contains__(), AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), AstRef.__deepcopy__(), Datatype.__deepcopy__(), ParamsRef.__deepcopy__(), ParamDescrsRef.__deepcopy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), AstMap.__deepcopy__(), FuncEntry.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), Statistics.__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__(), ArithRef.__div__(), BitVecRef.__div__(), ExprRef.__eq__(), ArithRef.__ge__(), BitVecRef.__ge__(), AstVector.__getitem__(), ModelRef.__getitem__(), Statistics.__getitem__(), AstMap.__getitem__(), ArithRef.__gt__(), BitVecRef.__gt__(), BitVecRef.__invert__(), ArithRef.__le__(), BitVecRef.__le__(), AstVector.__len__(), AstMap.__len__(), ModelRef.__len__(), Statistics.__len__(), BitVecRef.__lshift__(), ArithRef.__lt__(), BitVecRef.__lt__(), ArithRef.__mod__(), BitVecRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), BitVecRef.__mul__(), ExprRef.__ne__(), ArithRef.__neg__(), BitVecRef.__neg__(), BitVecRef.__or__(), ArithRef.__pow__(), ArithRef.__radd__(), BitVecRef.__radd__(), BitVecRef.__rand__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), ParamsRef.__repr__(), ParamDescrsRef.__repr__(), AstMap.__repr__(), Statistics.__repr__(), BitVecRef.__rlshift__(), ArithRef.__rmod__(), BitVecRef.__rmod__(), ArithRef.__rmul__(), BitVecRef.__rmul__(), BitVecRef.__ror__(), ArithRef.__rpow__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), ArithRef.__rsub__(), BitVecRef.__rsub__(), BitVecRef.__rxor__(), AstVector.__setitem__(), AstMap.__setitem__(), ArithRef.__sub__(), BitVecRef.__sub__(), BitVecRef.__xor__(), DatatypeSortRef.accessor(), ExprRef.arg(), FuncEntry.arg_value(), FuncInterp.arity(), Goal.as_expr(), Solver.assert_and_track(), Goal.assert_exprs(), Solver.assert_exprs(), QuantifierRef.body(), Solver.check(), Goal.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), ModelRef.decls(), ArrayRef.default(), RatNumRef.denominator(), Goal.depth(), Goal.dimacs(), FuncDeclRef.domain(), ArraySortRef.domain_n(), FuncInterp.else_value(), FuncInterp.entry(), AstMap.erase(), ModelRef.eval(), Goal.get(), ParamDescrsRef.get_documentation(), ModelRef.get_interp(), Statistics.get_key_value(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), ModelRef.get_sort(), ModelRef.get_universe(), Goal.inconsistent(), AstMap.keys(), Statistics.keys(), Solver.model(), SortRef.name(), QuantifierRef.no_pattern(), FuncEntry.num_args(), FuncInterp.num_entries(), Solver.num_scopes(), ModelRef.num_sorts(), FuncDeclRef.params(), QuantifierRef.pattern(), AlgebraicNumRef.poly(), Solver.pop(), Goal.prec(), ModelRef.project(), ModelRef.project_with_witness(), Solver.push(), AstVector.push(), QuantifierRef.qid(), FuncDeclRef.range(), ArraySortRef.range(), DatatypeSortRef.recognizer(), Context.ref(), AstMap.reset(), Solver.reset(), AstVector.resize(), Solver.set(), ParamsRef.set(), Goal.sexpr(), AstVector.sexpr(), ModelRef.sexpr(), ParamDescrsRef.size(), Goal.size(), QuantifierRef.skolem_id(), AstVector.translate(), AstRef.translate(), Goal.translate(), ModelRef.translate(), ExprRef.update(), ParamsRef.validate(), FuncEntry.value(), QuantifierRef.var_name(), and QuantifierRef.var_sort().

◆ fixedpoint

fixedpoint

Definition at line 7702 of file z3py.py.

◆ vars

vars

Definition at line 7708 of file z3py.py.

Public Member Functions

Data Fields

Additional Inherited Members