Package com.microsoft.z3

Class Goal

java.lang.Object
com.microsoft.z3.Z3Object
com.microsoft.z3.Goal
public class Goal extends Z3Object
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

  • Method Details

    • getPrecision

      public Z3_goal_prec getPrecision()
      The precision of the goal. Remarks: Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

    • isPrecise

      public boolean isPrecise()
      Indicates whether the goal is precise.

    • isUnderApproximation

      public boolean isUnderApproximation()
      Indicates whether the goal is an under-approximation.

    • isOverApproximation

      public boolean isOverApproximation()
      Indicates whether the goal is an over-approximation.

    • isGarbage

      public boolean isGarbage()
      Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).

    • add

      @SafeVarargs public final void add(Expr<BoolSort>... constraints)
      Adds the constraints to the given goal.
      Throws:
      Z3Exception

    • inconsistent

      public boolean inconsistent()
      Indicates whether the goal contains `false'.

    • getDepth

      public int getDepth()
      The depth of the goal. Remarks: This tracks how many transformations were applied to it.

    • reset

      public void reset()
      Erases all formulas from the given goal.

    • size

      public int size()
      The number of formulas in the goal.

    • getFormulas

      public BoolExpr[] getFormulas()
      The formulas in the goal.
      Throws:
      Z3Exception

    • getNumExprs

      public int getNumExprs()
      The number of formulas, subformulas and terms in the goal.

    • isDecidedSat

      public boolean isDecidedSat()
      Indicates whether the goal is empty, and it is precise or the product of an under approximation.

    • isDecidedUnsat

      public boolean isDecidedUnsat()
      Indicates whether the goal contains `false', and it is precise or the product of an over approximation.

    • translate

      public Goal translate(Context ctx)
      Translates (copies) the Goal to the target Context ctx.
      Throws:
      Z3Exception

    • simplify

      public Goal simplify()
      Simplifies the goal. Remarks: Essentially invokes the `simplify' tactic on the goal.

    • simplify

      public Goal simplify(Params p)
      Simplifies the goal. Remarks: Essentially invokes the `simplify' tactic on the goal.

    • toString

      public String toString()
      Goal to string conversion.
      Overrides:
      toString in class Object
      Returns:
      A string representation of the Goal.

    • AsBoolExpr

      public BoolExpr AsBoolExpr()
      Goal to BoolExpr conversion. Returns a string representation of the Goal.

    • convertModel

      public Model convertModel(Model m)
      Convert a model for the goal into a model of the original goal from which this goal was derived.
      Returns:
      A model for g
      Throws:
      Z3Exception