Z3
Public Member Functions
Goal Class Reference
+ Inheritance diagram for Goal:

Public Member Functions

Z3_goal_prec getPrecision () throws Z3Exception
 
boolean isPrecise () throws Z3Exception
 
boolean isUnderApproximation () throws Z3Exception
 
boolean isOverApproximation () throws Z3Exception
 
boolean isGarbage () throws Z3Exception
 
void add (BoolExpr...constraints) throws Z3Exception
 
boolean inconsistent () throws Z3Exception
 
int getDepth () throws Z3Exception
 
void reset () throws Z3Exception
 
int size () throws Z3Exception
 
BoolExpr[] getFormulas () throws Z3Exception
 
int getNumExprs () throws Z3Exception
 
boolean isDecidedSat () throws Z3Exception
 
boolean isDecidedUnsat () throws Z3Exception
 
Goal translate (Context ctx) throws Z3Exception
 
Goal simplify () throws Z3Exception
 
Goal simplify (Params p) throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

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) throws Z3Exception
inline

Adds the constraints to the given goal.

Exceptions
Z3Exception

Definition at line 79 of file Goal.java.

80  {
81  getContext().checkContextMatch(constraints);
82  for (BoolExpr c : constraints)
83  {
84  Native.goalAssert(getContext().nCtx(), getNativeObject(),
85  c.getNativeObject());
86  }
87  }
int getDepth ( ) throws Z3Exception
inline

The depth of the goal.

This tracks how many transformations were applied to it.

Definition at line 101 of file Goal.java.

102  {
103  return Native.goalDepth(getContext().nCtx(), getNativeObject());
104  }
BoolExpr [] getFormulas ( ) throws Z3Exception
inline

The formulas in the goal.

Exceptions
Z3Exception

Definition at line 127 of file Goal.java.

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

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

Definition at line 140 of file Goal.java.

141  {
142  return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
143  }
Z3_goal_prec getPrecision ( ) throws Z3Exception
inline

The precision of the goal.

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.

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

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

Indicates whether the goal contains `false'.

Definition at line 92 of file Goal.java.

93  {
94  return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
95  }
boolean isDecidedSat ( ) throws Z3Exception
inline

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

Definition at line 149 of file Goal.java.

150  {
151  return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
152  }
boolean isDecidedUnsat ( ) throws Z3Exception
inline

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

Definition at line 158 of file Goal.java.

159  {
160  return Native
161  .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
162  }
boolean isGarbage ( ) throws Z3Exception
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  {
72  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1221
Z3_goal_prec getPrecision()
Definition: Goal.java:35
boolean isOverApproximation ( ) throws Z3Exception
inline

Indicates whether the goal is an over-approximation.

Definition at line 60 of file Goal.java.

61  {
63  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1221
Z3_goal_prec getPrecision()
Definition: Goal.java:35
boolean isPrecise ( ) throws Z3Exception
inline

Indicates whether the goal is precise.

Definition at line 44 of file Goal.java.

45  {
47  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1221
Z3_goal_prec getPrecision()
Definition: Goal.java:35
boolean isUnderApproximation ( ) throws Z3Exception
inline

Indicates whether the goal is an under-approximation.

Definition at line 52 of file Goal.java.

53  {
55  }
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1221
Z3_goal_prec getPrecision()
Definition: Goal.java:35
void reset ( ) throws Z3Exception
inline

Erases all formulas from the given goal.

Definition at line 109 of file Goal.java.

110  {
111  Native.goalReset(getContext().nCtx(), getNativeObject());
112  }
Goal simplify ( ) throws Z3Exception
inline

Simplifies the goal.

Essentially invokes the `simplify' tactic on the goal.

Definition at line 180 of file Goal.java.

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

Simplifies the goal.

Essentially invokes the `simplify' tactic on the goal.

Definition at line 195 of file Goal.java.

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

The number of formulas in the goal.

Definition at line 117 of file Goal.java.

Referenced by Goal.getFormulas().

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

Goal to string conversion.

Returns
A string representation of the Goal.

Definition at line 211 of file Goal.java.

212  {
213  try
214  {
215  return Native.goalToString(getContext().nCtx(), getNativeObject());
216  } catch (Z3Exception e)
217  {
218  return "Z3Exception: " + e.getMessage();
219  }
220  }
Goal translate ( Context  ctx) throws Z3Exception
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  }