Z3 |

Public Member Functions
Goal Class Reference
Inheritance diagram for Goal:

## Public Member Functions
Z3_goal_prec | getPrecision ()
boolean | isPrecise ()
boolean | isUnderApproximation ()
boolean | isOverApproximation ()
boolean | isGarbage ()
final void | add (Expr< BoolSort >... constraints)
boolean | inconsistent ()
int | getDepth ()
void | reset ()
int | size ()
BoolExpr[] | getFormulas ()
int | getNumExprs ()
boolean | isDecidedSat ()
boolean | isDecidedUnsat ()
Goal | translate (Context ctx)
Goal | simplify ()
Goal | simplify (Params p)
String | toString ()
BoolExpr | AsBoolExpr ()
Model | convertModel (Model m)

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

Definition at line 26 of file Goal.java.

## Member Function Documentation

## ◆ add()

final void add | ( | Expr< BoolSort >... | constraints | ) |
| inline

Adds the `constraints` to the given goal.

Exceptions

  Z3Exception |

Definition at line 80 of file Goal.java.

81 {
82 getContext().checkContextMatch(constraints);
83 for (Expr<BoolSort> c : constraints)
84 {
85 Native.goalAssert(getContext().nCtx(), getNativeObject(),
86 c.getNativeObject());
87 }
88 }

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

## ◆ AsBoolExpr()

BoolExpr AsBoolExpr | ( |  | ) |
| inline

Goal to BoolExpr conversion.

Returns a string representation of the Goal.

Definition at line 222 of file Goal.java.

222 {
223 int n = size();
224 if (n == 0) {
225 return getContext().mkTrue();
226 } else if (n == 1) {
227 return getFormulas()[0];
228 } else {
229 return getContext().mkAnd(getFormulas());
230 }
231 }
com.microsoft.z3.Context.mkTrue
BoolExpr mkTrue()
Definition: Context.java:702
com.microsoft.z3.Context.mkAnd
final BoolExpr mkAnd(Expr< BoolSort >... t)
Definition: Context.java:807
com.microsoft.z3.Goal.getFormulas
BoolExpr[] getFormulas()
Definition: Goal.java:129
com.microsoft.z3.Goal.size
int size()
Definition: Goal.java:119

## ◆ convertModel()

Model convertModel | ( | Model | m | ) |
| inline

Convert a model for the goal into a model of the original goal from which this goal was derived.

Returns
  A model for `g`

Exceptions

  Z3Exception |

Definition at line 250 of file Goal.java.

251 {
252 return new Model(getContext(),
253 Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
254 }
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579

## ◆ getDepth()

int getDepth | ( |  | ) |
| inline

The depth of the goal. Remarks: This tracks how many transformations were applied to it.

Definition at line 103 of file Goal.java.

104 {
105 return Native.goalDepth(getContext().nCtx(), getNativeObject());
106 }

## ◆ getFormulas()

BoolExpr[] getFormulas | ( |  | ) |
| inline

The formulas in the goal.

Exceptions

  Z3Exception |

Definition at line 129 of file Goal.java.

130 {
131 int n = size();
132 BoolExpr[] res = new BoolExpr[n];
133 for (int i = 0; i < n; i++)
134 res[i] = (BoolExpr) Expr.create(getContext(), Native.goalFormula(getContext().nCtx(), getNativeObject(), i));
135 return res;
136 }

Referenced by Goal.AsBoolExpr().

## ◆ getNumExprs()

int getNumExprs | ( |  | ) |
| inline

The number of formulas, subformulas and terms in the goal.

Definition at line 141 of file Goal.java.

142 {
143 return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
144 }

## ◆ getPrecision()

Z3_goal_prec getPrecision | ( |  | ) |
| inline

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.

Definition at line 35 of file Goal.java.

36 {
37 return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
38 getNativeObject()));
39 }
Z3_goal_prec
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1408

Referenced by Goal.isGarbage(), Goal.isOverApproximation(), Goal.isPrecise(), and Goal.isUnderApproximation().

## ◆ inconsistent()

boolean inconsistent | ( |  | ) |
| inline

Indicates whether the goal contains ‘false’.

Definition at line 93 of file Goal.java.

94 {
95 return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
96 }

## ◆ isDecidedSat()

boolean isDecidedSat | ( |  | ) |
| inline

Indicates whether the goal is empty, and it is precise or the product of an under approximation.

Definition at line 150 of file Goal.java.

151 {
152 return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
153 }

## ◆ isDecidedUnsat()

boolean isDecidedUnsat | ( |  | ) |
| inline

Indicates whether the goal contains ‘false’, and it is precise or the product of an over approximation.

Definition at line 159 of file Goal.java.

160 {
161 return Native
162 .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
163 }

## ◆ isGarbage()

boolean isGarbage | ( |  | ) |
| inline

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

Definition at line 69 of file Goal.java.

70 {
71 return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
72 }
com.microsoft.z3.Goal.getPrecision
Z3_goal_prec getPrecision()
Definition: Goal.java:35

## ◆ isOverApproximation()

boolean isOverApproximation | ( |  | ) |
| inline

Indicates whether the goal is an over-approximation.

Definition at line 60 of file Goal.java.

61 {
62 return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
63 }

## ◆ isPrecise()

boolean isPrecise | ( |  | ) |
| inline

Indicates whether the goal is precise.

Definition at line 44 of file Goal.java.

45 {
46 return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
47 }

## ◆ isUnderApproximation()

boolean isUnderApproximation | ( |  | ) |
| inline

Indicates whether the goal is an under-approximation.

Definition at line 52 of file Goal.java.

53 {
54 return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
55 }

## ◆ reset()

void reset | ( |  | ) |
| inline

Erases all formulas from the given goal.

Definition at line 111 of file Goal.java.

112 {
113 Native.goalReset(getContext().nCtx(), getNativeObject());
114 }

## ◆ simplify() [1/2]

Goal simplify | ( |  | ) |
| inline

Simplifies the goal. Remarks: Essentially invokes the ‘simplify’ tactic on the goal.

Definition at line 181 of file Goal.java.

182 {
183 Tactic t = getContext().mkTactic("simplify");
184 ApplyResult res = t.apply(this);
185
186 if (res.getNumSubgoals() == 0)
187 throw new Z3Exception("No subgoals");
188 else
189 return res.getSubgoals()[0];
190 }
com.microsoft.z3.Context.mkTactic
Tactic mkTactic(String name)
Definition: Context.java:2757
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g)
Definition: Tactic.java:50

## ◆ simplify() [2/2]

Goal simplify | ( | Params | p | ) |
| inline

Simplifies the goal. Remarks: Essentially invokes the ‘simplify’ tactic on the goal.

Definition at line 197 of file Goal.java.

198 {
199 Tactic t = getContext().mkTactic("simplify");
200 ApplyResult res = t.apply(this, p);
201
202 if (res.getNumSubgoals() == 0)
203 throw new Z3Exception("No subgoals");
204 else
205 return res.getSubgoals()[0];
206 }

## ◆ size()

int size | ( |  | ) |
| inline

The number of formulas in the goal.

Definition at line 119 of file Goal.java.

120 {
121 return Native.goalSize(getContext().nCtx(), getNativeObject());
122 }

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Goal.AsBoolExpr(), Goal.getFormulas(), and BitVecSortRef.subsort().

## ◆ toString()

String toString | ( |  | ) |
| inline

Goal to string conversion.

Returns
  A string representation of the Goal.

Definition at line 213 of file Goal.java.

213 {
214 return Native.goalToString(getContext().nCtx(), getNativeObject());
215 }

## ◆ translate()

Goal translate | ( | Context | ctx | ) |
| inline

Translates (copies) the Goal to the target Context `ctx`.

Exceptions

  Z3Exception |

Definition at line 170 of file Goal.java.

171 {
172 return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
173 getNativeObject(), ctx.nCtx()));
174 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().