Z3
Data Structures | 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 28 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 82 of file Goal.java.

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

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 224 of file Goal.java.

224  {
225  int n = size();
226  if (n == 0) {
227  return getContext().mkTrue();
228  } else if (n == 1) {
229  return getFormulas()[0];
230  } else {
231  return getContext().mkAnd(getFormulas());
232  }
233  }
final BoolExpr mkAnd(Expr< BoolSort >... t)
Definition: Context.java:831
BoolExpr[] getFormulas()
Definition: Goal.java:131

◆ 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 252 of file Goal.java.

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

◆ getDepth()

int getDepth ( )
inline

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

Definition at line 105 of file Goal.java.

106  {
107  return Native.goalDepth(getContext().nCtx(), getNativeObject());
108  }

◆ getFormulas()

BoolExpr [] getFormulas ( )
inline

The formulas in the goal.

Exceptions
Z3Exception

Definition at line 131 of file Goal.java.

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

Referenced by Goal.AsBoolExpr().

◆ getNumExprs()

int getNumExprs ( )
inline

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

Definition at line 143 of file Goal.java.

144  {
145  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
146  }

◆ 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 37 of file Goal.java.

38  {
39  return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
40  getNativeObject()));
41  }
Z3_goal_prec
Z3 custom error handler (See Z3_set_error_handler).
Definition: z3_api.h:1390

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

◆ inconsistent()

boolean inconsistent ( )
inline

Indicates whether the goal contains ‘false’.

Definition at line 95 of file Goal.java.

96  {
97  return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
98  }

◆ isDecidedSat()

boolean isDecidedSat ( )
inline

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

Definition at line 152 of file Goal.java.

153  {
154  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
155  }

◆ isDecidedUnsat()

boolean isDecidedUnsat ( )
inline

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

Definition at line 161 of file Goal.java.

162  {
163  return Native
164  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
165  }

◆ isGarbage()

boolean isGarbage ( )
inline

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

Definition at line 71 of file Goal.java.

72  {
73  return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
74  }
Z3_goal_prec getPrecision()
Definition: Goal.java:37

◆ isOverApproximation()

boolean isOverApproximation ( )
inline

Indicates whether the goal is an over-approximation.

Definition at line 62 of file Goal.java.

63  {
64  return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
65  }

◆ isPrecise()

boolean isPrecise ( )
inline

Indicates whether the goal is precise.

Definition at line 46 of file Goal.java.

47  {
48  return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
49  }

◆ isUnderApproximation()

boolean isUnderApproximation ( )
inline

Indicates whether the goal is an under-approximation.

Definition at line 54 of file Goal.java.

55  {
56  return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
57  }

◆ reset()

void reset ( )
inline

Erases all formulas from the given goal.

Definition at line 113 of file Goal.java.

114  {
115  Native.goalReset(getContext().nCtx(), getNativeObject());
116  }

◆ simplify() [1/2]

Goal simplify ( )
inline

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

Definition at line 183 of file Goal.java.

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

◆ simplify() [2/2]

Goal simplify ( Params  p)
inline

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

Definition at line 199 of file Goal.java.

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

◆ size()

int size ( )
inline

The number of formulas in the goal.

Definition at line 121 of file Goal.java.

122  {
123  return Native.goalSize(getContext().nCtx(), getNativeObject());
124  }

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 215 of file Goal.java.

215  {
216  return Native.goalToString(getContext().nCtx(), getNativeObject());
217  }

◆ translate()

Goal translate ( Context  ctx)
inline

Translates (copies) the Goal to the target Context

ctx

.

Exceptions
Z3Exception

Definition at line 172 of file Goal.java.

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

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__().