Z3
Goal.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_goal_prec;
21
26public class Goal extends Z3Object {
36 {
37 return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
38 getNativeObject()));
39 }
40
44 public boolean isPrecise()
45 {
46 return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
47 }
48
52 public boolean isUnderApproximation()
53 {
54 return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
55 }
56
60 public boolean isOverApproximation()
61 {
62 return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
63 }
64
69 public boolean isGarbage()
70 {
71 return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
72 }
73
79 @SafeVarargs
80 public final void add(Expr<BoolSort>... constraints)
81 {
82 getContext().checkContextMatch(constraints);
83 for (Expr<BoolSort> c : constraints)
84 {
85 Native.goalAssert(getContext().nCtx(), getNativeObject(),
86 c.getNativeObject());
87 }
88 }
89
93 public boolean inconsistent()
94 {
95 return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
96 }
97
103 public int getDepth()
104 {
105 return Native.goalDepth(getContext().nCtx(), getNativeObject());
106 }
107
111 public void reset()
112 {
113 Native.goalReset(getContext().nCtx(), getNativeObject());
114 }
115
119 public int size()
120 {
121 return Native.goalSize(getContext().nCtx(), getNativeObject());
122 }
123
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 }
137
141 public int getNumExprs()
142 {
143 return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
144 }
145
150 public boolean isDecidedSat()
151 {
152 return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
153 }
154
159 public boolean isDecidedUnsat()
160 {
161 return Native
162 .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
163 }
164
171 {
172 return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
173 getNativeObject(), ctx.nCtx()));
174 }
175
181 public Goal simplify()
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 }
191
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 }
207
213 public String toString() {
214 return Native.goalToString(getContext().nCtx(), getNativeObject());
215 }
216
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 }
232
233 Goal(Context ctx, long obj)
234 {
235 super(ctx, obj);
236 }
237
238 Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) {
239 super(ctx, Native.mkGoal(ctx.nCtx(), (models),
240 (unsatCores), (proofs)));
241 }
242
251 {
252 return new Model(getContext(),
253 Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
254 }
255
256
257
258 @Override
259 void incRef() {
260 Native.goalIncRef(getContext().nCtx(), getNativeObject());
261 }
262
263 @Override
264 void addToReferenceQueue() {
265 getContext().getGoalDRQ().storeReference(getContext(), this);
266 }
267}
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4100
Tactic mkTactic(String name)
Definition: Context.java:2757
final BoolExpr mkAnd(Expr< BoolSort >... t)
Definition: Context.java:807
boolean isOverApproximation()
Definition: Goal.java:60
boolean isUnderApproximation()
Definition: Goal.java:52
boolean isGarbage()
Definition: Goal.java:69
boolean isPrecise()
Definition: Goal.java:44
BoolExpr AsBoolExpr()
Definition: Goal.java:222
Z3_goal_prec getPrecision()
Definition: Goal.java:35
final void add(Expr< BoolSort >... constraints)
Definition: Goal.java:80
Goal translate(Context ctx)
Definition: Goal.java:170
boolean isDecidedUnsat()
Definition: Goal.java:159
Goal simplify(Params p)
Definition: Goal.java:197
Model convertModel(Model m)
Definition: Goal.java:250
String toString()
Definition: Goal.java:213
BoolExpr[] getFormulas()
Definition: Goal.java:129
boolean inconsistent()
Definition: Goal.java:93
boolean isDecidedSat()
Definition: Goal.java:150
void storeReference(Context ctx, T obj)
ApplyResult apply(Goal g)
Definition: Tactic.java:50
def String(name, ctx=None)
Definition: z3py.py:10693
def Model(ctx=None)
Definition: z3py.py:6579
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1408