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 ()
 
Model convertModel (Model m)
 

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

void add ( BoolExpr ...  constraints)
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 }

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

221 {
222 int n = size();
223 if (n == 0) {
224 return getContext().mkTrue();
225 } else if (n == 1) {
226 return getFormulas()[0];
227 } else {
228 return getContext().mkAnd(getFormulas());
229 }
230 }
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:780
BoolExpr[] getFormulas()
Definition: Goal.java:128

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

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

◆ getDepth()

int getDepth ( )
inline

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

Definition at line 102 of file Goal.java.

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

◆ getFormulas()

BoolExpr[] getFormulas ( )
inline

The formulas in the goal.

Exceptions
Z3Exception

Definition at line 128 of file Goal.java.

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

Referenced by Goal.AsBoolExpr().

◆ getNumExprs()

int getNumExprs ( )
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 }

◆ 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
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1401

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

◆ inconsistent()

boolean inconsistent ( )
inline

Indicates whether the goal contains ‘false’.

Definition at line 92 of file Goal.java.

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

◆ isDecidedSat()

boolean isDecidedSat ( )
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 }

◆ isDecidedUnsat()

boolean isDecidedUnsat ( )
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 }

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

◆ isOverApproximation()

boolean isOverApproximation ( )
inline

Indicates whether the goal is an over-approximation.

Definition at line 60 of file Goal.java.

◆ isPrecise()

boolean isPrecise ( )
inline

Indicates whether the goal is precise.

Definition at line 44 of file Goal.java.

◆ isUnderApproximation()

boolean isUnderApproximation ( )
inline

Indicates whether the goal is an under-approximation.

Definition at line 52 of file Goal.java.

◆ reset()

void reset ( )
inline

Erases all formulas from the given goal.

Definition at line 110 of file Goal.java.

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

◆ simplify() [1/2]

Goal simplify ( )
inline

Simplifies the goal. Remarks: 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 }
Tactic mkTactic(String name)
Definition: Context.java:2715
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 196 of file Goal.java.

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

◆ size()

int size ( )
inline

The number of formulas in the goal.

Definition at line 118 of file Goal.java.

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

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

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

◆ translate()

Goal translate ( Context  ctx)
inline

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

Exceptions
Z3Exception

Definition at line 169 of file Goal.java.

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

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