Z3FixedPoint

public class Z3FixedPoint : Z3RefCountedObject

Context for the recursive predicate solver.

  • Declaration

    Swift

    public let context: Z3Context

  • Add a universal Horn clause as a named rule. The horn_rule should be of the form:

    horn_rule ::= (forall (bound-vars) horn_rule)
           |  (=> atoms horn_rule)
           |  atom

    Declaration

    Swift

    public func addRule(_ rule: Z3Bool, name: Z3Symbol? = nil)

  • Add a Database fact.

    The number of arguments in args should be equal to the number of sorts in the domain of predicate. 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

    Declaration

    Swift

    public func query(_ query: Z3Bool) -> Z3LBool

    Return Value

    • Z3LBool.lFalse: if the query is unsatisfiable.
    • Z3LBool.lTrue: if the query is satisfiable. Obtain the answer by calling getAnswer().
    • 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 calling getAnswer().
    • 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 returned Z3LBool.lTrue. When used with the PDR engine, the previous call must have been either Z3LBool.lTrue or Z3LBool.lFalse.

    Declaration

    Swift

    public func getAnswer() -> AnyZ3Ast

  • Retrieve a string that describes the last status returned by query(_:).

    Use this method when query(_:) returns Z3LBool.lUndef.

    Declaration

    Swift

    public func getReasonUnknown() -> String

  • Update a named rule. A rule with the same name must have been previously created.

    Seealso

    addRule(_:name:)

    Declaration

    Swift

    public func updateRule(_ rule: Z3Bool, name: Z3Symbol)

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

  • Retrieve statistics information from the last call to query(_:)

    Declaration

    Swift

    public func getStatistics() -> Z3Stats

  • \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

  • Set parameters on fixedpoint context.

    Seealso

    getHelp()

    Seealso

    getParamDescrs()

    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