Package com.microsoft.z3

Class Fixedpoint

java.lang.Object
com.microsoft.z3.Z3Object
com.microsoft.z3.Fixedpoint
public class Fixedpoint extends Z3Object
Object for managing fixedpoints

  • Method Details

    • getHelp

      public String getHelp()
      A string that describes all available fixedpoint solver parameters.

    • setParameters

      public void setParameters(Params value)
      Sets the fixedpoint solver parameters.
      Throws:
      Z3Exception

    • getParameterDescriptions

      public ParamDescrs getParameterDescriptions()
      Retrieves parameter descriptions for Fixedpoint solver.
      Throws:
      Z3Exception

    • add

      @SafeVarargs public final void add(Expr<BoolSort>... constraints)
      Assert a constraint (or multiple) into the fixedpoint solver.
      Throws:
      Z3Exception

    • registerRelation

      public void registerRelation(FuncDecl<BoolSort> f)
      Register predicate as recursive relation.
      Throws:
      Z3Exception

    • addRule

      public void addRule(Expr<BoolSort> rule, Symbol name)
      Add rule into the fixedpoint solver.
      Parameters:
      rule - implication (Horn clause) representing rule
      name - Nullable rule name.
      Throws:
      Z3Exception

    • addFact

      public void addFact(FuncDecl<BoolSort> pred, int... args)
      Add table fact to the fixedpoint solver.
      Throws:
      Z3Exception

    • query

      public Status query(Expr<BoolSort> query)
      Query the fixedpoint solver. A query is a conjunction of constraints. The constraints may include the recursively defined relations. The query is satisfiable if there is an instance of the query variables and a derivation for it. The query is unsatisfiable if there are no derivations satisfying the query variables.
      Throws:
      Z3Exception

    • query

      public Status query(FuncDecl<BoolSort>[] relations)
      Query the fixedpoint solver. A query is an array of relations. The query is satisfiable if there is an instance of some relation that is non-empty. The query is unsatisfiable if there are no derivations satisfying any of the relations.
      Throws:
      Z3Exception

    • updateRule

      public void updateRule(Expr<BoolSort> rule, Symbol name)
      Update named rule into in the fixedpoint solver.
      Parameters:
      rule - implication (Horn clause) representing rule
      name - Nullable rule name.
      Throws:
      Z3Exception

    • getAnswer

      public Expr<?> getAnswer()
      Retrieve satisfying instance or instances of solver, or definitions for the recursive predicates that show unsatisfiability.
      Throws:
      Z3Exception

    • getReasonUnknown

      public String getReasonUnknown()
      Retrieve explanation why fixedpoint engine returned status Unknown.

    • getNumLevels

      public int getNumLevels(FuncDecl<BoolSort> predicate)
      Retrieve the number of levels explored for a given predicate.

    • getCoverDelta

      public Expr<?> getCoverDelta(int level, FuncDecl<BoolSort> predicate)
      Retrieve the cover of a predicate.
      Throws:
      Z3Exception

    • addCover

      public void addCover(int level, FuncDecl<BoolSort> predicate, Expr<?> property)
      Add property about the predicate. The property is added at level.

    • toString

      public String toString()
      Retrieve internal string representation of fixedpoint object.
      Overrides:
      toString in class Object

    • setPredicateRepresentation

      public void setPredicateRepresentation(FuncDecl<BoolSort> f, Symbol[] kinds)
      Instrument the Datalog engine on which table representation to use for recursive predicate.

    • toString

      public String toString(Expr<BoolSort>[] queries)
      Convert benchmark given as set of axioms, rules and queries to a string.

    • getRules

      public BoolExpr[] getRules()
      Retrieve set of rules added to fixedpoint context.
      Throws:
      Z3Exception

    • getAssertions

      public BoolExpr[] getAssertions()
      Retrieve set of assertions added to fixedpoint context.
      Throws:
      Z3Exception

    • getStatistics

      public Statistics getStatistics()
      Fixedpoint statistics.
      Throws:
      Z3Exception

    • ParseFile

      public BoolExpr[] ParseFile(String file)
      Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.

    • ParseString

      public BoolExpr[] ParseString(String s)
      Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.