Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
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

Data Fields

 ctx
 fixedpoint
 vars

Detailed Description

Fixedpoint.

Fixedpoint API provides methods for solving with recursive predicates

Definition at line 6091 of file z3py.py.


Constructor & Destructor Documentation

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

Definition at line 6094 of file z3py.py.

06094 
06095     def __init__(self, fixedpoint=None, ctx=None):
06096         assert fixedpoint == None or ctx != None
06097         self.ctx    = _get_ctx(ctx)
06098         self.fixedpoint = None
06099         if fixedpoint == None:
06100             self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
06101         else:
06102             self.fixedpoint = fixedpoint
06103         Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint)
06104         self.vars = []

def __del__ (   self)

Definition at line 6105 of file z3py.py.

06105 
06106     def __del__(self):
06107         if self.fixedpoint != None:
06108             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 6269 of file z3py.py.

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

def abstract (   self,
  fml,
  is_forall = True 
)

Definition at line 6305 of file z3py.py.

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

06305 
06306     def abstract(self, fml, is_forall=True):
06307         if self.vars == []:
06308             return fml
06309         if is_forall:
06310             return ForAll(self.vars, fml)
06311         else:
06312             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 6137 of file z3py.py.

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

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

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

06149 
06150     def add_rule(self, head, body = None, name = None):
06151         """Assert rules defining recursive predicates to the fixedpoint solver.
06152         >>> a = Bool('a')
06153         >>> b = Bool('b')
06154         >>> s = Fixedpoint()
06155         >>> s.register_relation(a.decl())
06156         >>> s.register_relation(b.decl())
06157         >>> s.fact(a)
06158         >>> s.rule(b, a)
06159         >>> s.query(b)
06160         sat
06161         """
06162         if name == None:
06163             name = ""
06164         name = to_symbol(name, self.ctx)
06165         if body == None:
06166             head = self.abstract(head)
06167             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)            
06168         else:
06169             body = _get_args(body)
06170             f    = self.abstract(Implies(And(body),head))
06171             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 6141 of file z3py.py.

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

def assert_exprs (   self,
  args 
)
Assert constraints as background axioms for the fixedpoint solver.

Definition at line 6123 of file z3py.py.

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

06123 
06124     def assert_exprs(self, *args):
06125         """Assert constraints as background axioms for the fixedpoint solver."""
06126         args = _get_args(args)
06127         s    = BoolSort(self.ctx)
06128         for arg in args:
06129             if isinstance(arg, Goal) or isinstance(arg, AstVector):
06130                 for f in arg:
06131                     f = self.abstract(f)
06132                     Z3_fixedpoint_assert(self.ctx.ref(), self.fixedpoint, f.as_ast())
06133             else:
06134                 arg = s.cast(arg)
06135                 arg = self.abstract(arg)
06136                 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 6296 of file z3py.py.

06296 
06297     def declare_var(self, *vars):
06298         """Add variable or several variables.
06299         The added variable or variables will be bound in the rules
06300         and queries
06301         """
06302         vars = _get_args(vars)
06303         for v in vars:
06304             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 6176 of file z3py.py.

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

def get_answer (   self)
Retrieve answer from last query call.

Definition at line 6219 of file z3py.py.

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

def get_assertions (   self)
retrieve assertions that have been added to fixedpoint context

Definition at line 6265 of file z3py.py.

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

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

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

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

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

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

def param_descrs (   self)
Return the parameter description set.

Definition at line 6119 of file z3py.py.

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

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

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

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

def push (   self)
create a backtracking point for added rules, facts and assertions

Definition at line 6202 of file z3py.py.

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

06180 
06181     def query(self, *query):
06182         """Query the fixedpoint engine whether formula is derivable.
06183            You can also pass an tuple or list of recursive predicates.
06184         """
06185         query = _get_args(query)
06186         sz = len(query)
06187         if sz >= 1 and isinstance(query[0], FuncDecl):            
06188             _decls = (FuncDecl * sz)()
06189             i = 0
06190             for q in query:
06191                 _decls[i] = q.ast
06192                 i = i + 1
06193             r = Z3_fixedpoint_query_relations(self.ctx.ref(), self.fixedpoint, sz, _decls)
06194         else:
06195             if sz == 1:
06196                 query = query[0]
06197             else:
06198                 query = And(query)
06199             query = self.abstract(query, False)
06200             r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
06201         return CheckSatResult(r)

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

Definition at line 6291 of file z3py.py.

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

def register_relation (   self,
  relations 
)
Register relation as recursive

Definition at line 6237 of file z3py.py.

06237 
06238     def register_relation(self, *relations):
06239         """Register relation as recursive"""
06240         relations = _get_args(relations)
06241         for f in relations:
06242             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 6172 of file z3py.py.

06172 
06173     def rule(self, head, body = None, name = None):
06174         """Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
06175         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 6109 of file z3py.py.

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

06243 
06244     def set_predicate_representation(self, f, *representations):
06245         """Control how relation is represented"""
06246         representations = _get_args(representations)
06247         representations = [to_symbol(s) for s in representations]
06248         sz = len(representations)
06249         args = (Symbol * sz)()
06250         for i in range(sz):
06251             args[i] = representations[i]
06252         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 6273 of file z3py.py.

Referenced by Fixedpoint.__repr__().

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

06286 
06287     def statistics(self):
06288         """Return statistics for the last `query()`.
06289         """
06290         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 6278 of file z3py.py.

06278 
06279     def to_string(self, queries):
06280         """Return a formatted string (in Lisp-like format) with all added constraints.
06281            We say the string is in s-expression format.
06282            Include also queries.
06283         """
06284         args, len = _to_ast_array(queries)
06285         return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
    
def update_rule (   self,
  head,
  body,
  name 
)
update rule

Definition at line 6210 of file z3py.py.

06210 
06211     def update_rule(self, head, body, name):
06212         """update rule"""
06213         if name == None:
06214             name = ""
06215         name = to_symbol(name, self.ctx)
06216         body = _get_args(body)
06217         f    = self.abstract(Implies(And(body),head))
06218         Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)


Field Documentation

ctx

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

Definition at line 6094 of file z3py.py.

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

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines