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  }

◆ 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  }

◆ 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  }

◆ 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  }

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  }

◆ 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  }

◆ 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 Goal.AsBoolExpr(), and Goal.getFormulas().

◆ 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  }
com.microsoft.z3.Tactic.apply
ApplyResult apply(Goal g)
Definition: Tactic.java:50
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:1406
com.microsoft.z3.Goal.size
int size()
Definition: Goal.java:119
com.microsoft.z3.Context.mkTactic
Tactic mkTactic(String name)
Definition: Context.java:2741
com.microsoft.z3.Context.mkAnd
BoolExpr mkAnd(Expr< BoolSort >... t)
Definition: Context.java:803
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6277
com.microsoft.z3.ApplyResult.getSubgoals
Goal[] getSubgoals()
Definition: ApplyResult.java:39
com.microsoft.z3.Goal.getFormulas
BoolExpr[] getFormulas()
Definition: Goal.java:129
com.microsoft.z3.Goal.getPrecision
Z3_goal_prec getPrecision()
Definition: Goal.java:35
com.microsoft.z3.Context.mkTrue
BoolExpr mkTrue()
Definition: Context.java:700