Package com.microsoft.z3

Class Solver

java.lang.Object
com.microsoft.z3.Z3Object
com.microsoft.z3.Solver
public class Solver extends Z3Object
Solvers.

  • Method Details

    • getHelp

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

    • setParameters

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

    • getParameterDescriptions

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

    • getNumScopes

      public int getNumScopes()
      The current number of backtracking points (scopes).
      See Also:

    • push

      public void push()
      Creates a backtracking point.
      See Also:

    • pop

      public void pop()
      Backtracks one backtracking point. Remarks: .

    • pop

      public void pop(int n)
      Backtracks n backtracking points. Remarks: Note that an exception is thrown if n is not smaller than NumScopes
      See Also:

    • reset

      public void reset()
      Resets the Solver. Remarks: This removes all assertions from the solver.

    • interrupt

      public void interrupt()
      Interrupt the execution of the solver object. Remarks: This ensures that the interrupt applies only to the given solver object and it applies only if it is running.

    • add

      public void add(Expr<BoolSort>... constraints)
      Assert a multiple constraints into the solver.
      Throws:
      Z3Exception

    • assertAndTrack

      public void assertAndTrack(Expr<BoolSort>[] constraints, Expr<BoolSort>[] ps)
      Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps. Remarks: This API is an alternative to check() with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using #assertAndTrack and the Boolean literals provided using check() with assumptions.

    • assertAndTrack

      public void assertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
      Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p. Remarks: This API is an alternative to check(com.microsoft.z3.Expr<com.microsoft.z3.BoolSort>...) with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using assertAndTrack(com.microsoft.z3.Expr<com.microsoft.z3.BoolSort>[], com.microsoft.z3.Expr<com.microsoft.z3.BoolSort>[]) and the Boolean literals provided using check(com.microsoft.z3.Expr<com.microsoft.z3.BoolSort>...) with assumptions.

    • fromFile

      public void fromFile(String file)

    • fromString

      public void fromString(String str)

    • getNumAssertions

      public int getNumAssertions()
      The number of assertions in the solver.
      Throws:
      Z3Exception

    • getAssertions

      public BoolExpr[] getAssertions()
      The set of asserted formulas.
      Throws:
      Z3Exception

    • check

      @SafeVarargs public final Status check(Expr<BoolSort>... assumptions)
      Checks whether the assertions in the solver are consistent or not. Remarks:
      See Also:

    • check

      public Status check()
      Checks whether the assertions in the solver are consistent or not. Remarks:
      See Also:

    • getConsequences

      public Status getConsequences(Expr<BoolSort>[] assumptions, Expr<?>[] variables, List<Expr<BoolSort>> consequences)
      Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is an implication of the form relevant-assumptions Implies variable = value where the relevant assumptions is a subset of the assumptions that are passed in and the equality on the right side of the implication indicates how a variable is fixed.

    • getModel

      public Model getModel()
      The model of the last Check. Remarks: The result is null if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.
      Throws:
      Z3Exception

    • getProof

      public Expr<?> getProof()
      The proof of the last Check. Remarks: The result is null if Check was not invoked before, if its results was not UNSATISFIABLE, or if proof production is disabled.
      Throws:
      Z3Exception

    • getUnsatCore

      public BoolExpr[] getUnsatCore()
      The unsat core of the last Check. Remarks: The unsat core is a subset of Assertions The result is empty if Check was not invoked before, if its results was not UNSATISFIABLE, or if core production is disabled.
      Throws:
      Z3Exception

    • getReasonUnknown

      public String getReasonUnknown()
      A brief justification of why the last call to Check returned UNKNOWN.

    • translate

      public Solver translate(Context ctx)
      Create a clone of the current solver with respect toctx.

    • getStatistics

      public Statistics getStatistics()
      Solver statistics.
      Throws:
      Z3Exception

    • toString

      public String toString()
      A string representation of the solver.
      Overrides:
      toString in class Object