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 ()
 
void add (BoolExpr...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 ()
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

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

void add ( BoolExpr...  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 (BoolExpr c : constraints)
84  {
85  Native.goalAssert(getContext().nCtx(), getNativeObject(),
86  c.getNativeObject());
87  }
88  }
BoolExpr AsBoolExpr ( )
inline

Goal to BoolExpr conversion.

Returns a string representation of the Goal.

Definition at line 230 of file Goal.java.

230  {
231  int n = size();
232  if (n == 0)
233  return getContext().mkTrue();
234  else if (n == 1)
235  return getFormulas()[0];
236  else {
237  return getContext().mkAnd(getFormulas());
238  }
239  }
BoolExpr mkAnd(BoolExpr...t)
Definition: Context.java:723
BoolExpr[] getFormulas()
Definition: Goal.java:129
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  }
BoolExpr [] getFormulas ( )
inline

The formulas in the goal.

Exceptions
Z3Exception

Definition at line 129 of file Goal.java.

Referenced by Goal.AsBoolExpr().

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

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

Definition at line 142 of file Goal.java.

143  {
144  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
145  }
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 36 of file Goal.java.

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

37  {
38  return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
39  getNativeObject()));
40  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1385
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  }
boolean isDecidedSat ( )
inline

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

Definition at line 151 of file Goal.java.

152  {
153  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
154  }
boolean isDecidedUnsat ( )
inline

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

Definition at line 160 of file Goal.java.

161  {
162  return Native
163  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
164  }
boolean isGarbage ( )
inline

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

Definition at line 70 of file Goal.java.

71  {
73  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1385
Z3_goal_prec getPrecision()
Definition: Goal.java:36
boolean isOverApproximation ( )
inline

Indicates whether the goal is an over-approximation.

Definition at line 61 of file Goal.java.

62  {
64  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1385
Z3_goal_prec getPrecision()
Definition: Goal.java:36
boolean isPrecise ( )
inline

Indicates whether the goal is precise.

Definition at line 45 of file Goal.java.

46  {
48  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1385
Z3_goal_prec getPrecision()
Definition: Goal.java:36
boolean isUnderApproximation ( )
inline

Indicates whether the goal is an under-approximation.

Definition at line 53 of file Goal.java.

54  {
56  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1385
Z3_goal_prec getPrecision()
Definition: Goal.java:36
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  }
Goal simplify ( )
inline

Simplifies the goal. Remarks: Essentially invokes the `simplify' tactic on the goal.

Definition at line 182 of file Goal.java.

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

Simplifies the goal. Remarks: Essentially invokes the `simplify' tactic on the goal.

Definition at line 198 of file Goal.java.

199  {
200  Tactic t = getContext().mkTactic("simplify");
201  ApplyResult res = t.apply(this, p);
202 
203  if (res.getNumSubgoals() == 0)
204  throw new Z3Exception("No subgoals");
205  else
206  return res.getSubgoals()[0];
207  }
ApplyResult apply(Goal g)
Definition: Tactic.java:51
Tactic mkTactic(String name)
Definition: Context.java:2392
int size ( )
inline

The number of formulas in the goal.

Definition at line 119 of file Goal.java.

Referenced by Goal.AsBoolExpr(), and Goal.getFormulas().

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

Goal to string conversion.

Returns
A string representation of the Goal.

Definition at line 214 of file Goal.java.

215  {
216  try
217  {
218  return Native.goalToString(getContext().nCtx(), getNativeObject());
219  } catch (Z3Exception e)
220  {
221  return "Z3Exception: " + e.getMessage();
222  }
223  }
Goal translate ( Context  ctx)
inline

Translates (copies) the Goal to the target Context

ctx

.

Exceptions
Z3Exception

Definition at line 171 of file Goal.java.

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