Z3FixedPoint
public class Z3FixedPoint : Z3RefCountedObject
Context for the recursive predicate solver.
-
Declaration
Swift
public let context: Z3Context
-
Add a Database fact.
The number of arguments in
args
should be equal to the number of sorts in the domain ofpredicate
. Each sort in the domain should be an integral (bit-vector, Boolean or or finite domain sort).The call has the same effect as adding a rule where
predicate
is applied to the arguments.Declaration
Swift
public func addFact(_ predicate: Z3FuncDecl, args: [UInt32])
Parameters
predicate
- relation signature for the row.
args
- array of the row elements.
-
Assert a constraint to the fixedpoint context.
The constraints are used as background axioms when the fixedpoint engine uses the PDR mode. They are ignored for standard Datalog mode.
Declaration
Swift
public func assert(_ axiom: Z3Bool)
-
Pose a query against the asserted rules.
query ::= (exists (bound-vars) query) | literals
Return Value
Z3LBool.lFalse
: if the query is unsatisfiable.Z3LBool.lTrue
: if the query is satisfiable. Obtain the answer by callinggetAnswer()
.Z3LBool.lUndef
: if the query was interrupted, timed out or otherwise failed.
-
Pose multiple queries against the asserted rules.
The queries are encoded as relations (function declarations).
Declaration
Swift
public func query(_ relations: [Z3FuncDecl]) -> Z3LBool
Return Value
Z3LBool.lFalse
: if the query is unsatisfiable.Z3LBool.lTrue
: if the query is satisfiable. Obtain the answer by callinggetAnswer()
.Z3LBool.lUndef
: if the query was interrupted, timed out or otherwise failed.
-
Retrieve a formula that encodes satisfying answers to the query.
When used in Datalog mode, the returned answer is a disjunction of conjuncts. Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction.
When used in Datalog mode the previous call to
query(_:)
must have returnedZ3LBool.lTrue
. When used with the PDR engine, the previous call must have been eitherZ3LBool.lTrue
orZ3LBool.lFalse
.Declaration
Swift
public func getAnswer() -> AnyZ3Ast
-
Update a named rule. A rule with the same name must have been previously created.
Seealso
addRule(_:name:)
-
Query the PDR engine for the maximal levels properties are known about predicate.
This call retrieves the maximal number of relevant unfoldings of \c pred with respect to the current exploration state. Note: this functionality is PDR specific.
Declaration
Swift
public func getNumLevels(_ predicate: Z3FuncDecl) -> UInt32
-
Retrieve the current cover of \c pred up to \c level unfoldings. Return just the delta that is known at \c level. To obtain the full set of properties of \c pred one should query at \c level+1 , \c level+2 etc, and include \c level=-1.
Note: this functionality is PDR specific.
Declaration
Swift
public func getCoverDelta(level: Int, predicate: Z3FuncDecl) -> AnyZ3Ast
-
Retrieve the current cover of \c pred up to \c level unfoldings. Return just the delta that is known at \c level. To obtain the full set of properties of \c pred one should query at \c level+1 , \c level+2 etc, and include \c level=-1.
Note: this functionality is PDR specific.
Declaration
Swift
public func addCover(level: Int, predicate: Z3FuncDecl, property: AnyZ3Ast)
-
\brief Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.
Declaration
Swift
public func registerRelation(_ decl: Z3FuncDecl)
-
Configure the predicate representation.
It sets the predicate to use a set of domains given by the list of symbols. The domains given by the list of symbols must belong to a set of built-in domains.
Declaration
Swift
public func setPredicateRepresentation(_ f: Z3FuncDecl, kinds: [Z3Symbol])
-
Retrieve set of rules from fixedpoint context.
Declaration
Swift
public func getRules() -> Z3AstVector
-
Retrieve set of background assertions from fixedpoint context.
Declaration
Swift
public func getAssertions() -> Z3AstVector
-
Declaration
Swift
public func setParams(_ p: Z3Params)
-
Return a string describing all fixedpoint available parameters.
Seealso
getParamDescrs()
Seealso
setParams(_:)
Declaration
Swift
public func getHelp() -> String
-
Return the parameter description set for the given fixedpoint object.
Seealso
getHelp()
Seealso
setParams(_:)
Declaration
Swift
public func getParamDescrs() -> Z3ParamDescrs