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 {
47 }
48
52 public boolean isUnderApproximation()
53 {
55 }
56
60 public boolean isOverApproximation()
61 {
63 }
64
69 public boolean isGarbage()
70 {
72 }
73
79 public void add(BoolExpr ... constraints)
80 {
81 getContext().checkContextMatch(constraints);
82 for (BoolExpr c : constraints)
83 {
84 Native.goalAssert(getContext().nCtx(), getNativeObject(),
85 c.getNativeObject());
86 }
87 }
88
92 public boolean inconsistent()
93 {
94 return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
95 }
96
102 public int getDepth()
103 {
104 return Native.goalDepth(getContext().nCtx(), getNativeObject());
105 }
106
110 public void reset()
111 {
112 Native.goalReset(getContext().nCtx(), getNativeObject());
113 }
114
118 public int size()
119 {
120 return Native.goalSize(getContext().nCtx(), getNativeObject());
121 }
122
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 }
136
140 public int getNumExprs()
141 {
142 return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
143 }
144
149 public boolean isDecidedSat()
150 {
151 return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
152 }
153
158 public boolean isDecidedUnsat()
159 {
160 return Native
161 .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
162 }
163
170 {
171 return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
172 getNativeObject(), ctx.nCtx()));
173 }
174
180 public Goal simplify()
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 }
190
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 }
206
212 public String toString() {
213 return Native.goalToString(getContext().nCtx(), getNativeObject());
214 }
215
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 }
231
232 Goal(Context ctx, long obj)
233 {
234 super(ctx, obj);
235 }
236
237 Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs) {
238 super(ctx, Native.mkGoal(ctx.nCtx(), (models),
239 (unsatCores), (proofs)));
240 }
241
250 {
251 return new Model(getContext(),
252 Native.goalConvertModel(getContext().nCtx(), getNativeObject(), m.getNativeObject()));
253 }
254
255
256
257 @Override
258 void incRef() {
259 Native.goalIncRef(getContext().nCtx(), getNativeObject());
260 }
261
262 @Override
263 void addToReferenceQueue() {
264 getContext().getGoalDRQ().storeReference(getContext(), this);
265 }
266}
IDecRefQueue< Goal > getGoalDRQ()
Definition: Context.java:4058
BoolExpr mkAnd(BoolExpr... t)
Definition: Context.java:780
Tactic mkTactic(String name)
Definition: Context.java:2715
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:221
Z3_goal_prec getPrecision()
Definition: Goal.java:35
Goal translate(Context ctx)
Definition: Goal.java:169
boolean isDecidedUnsat()
Definition: Goal.java:158
Goal simplify(Params p)
Definition: Goal.java:196
Model convertModel(Model m)
Definition: Goal.java:249
String toString()
Definition: Goal.java:212
BoolExpr[] getFormulas()
Definition: Goal.java:128
boolean inconsistent()
Definition: Goal.java:92
void add(BoolExpr ... constraints)
Definition: Goal.java:79
boolean isDecidedSat()
Definition: Goal.java:149
void storeReference(Context ctx, T obj)
static boolean goalIsDecidedSat(long a0, long a1)
Definition: Native.java:4050
static boolean goalInconsistent(long a0, long a1)
Definition: Native.java:3997
static void goalReset(long a0, long a1)
Definition: Native.java:4015
static void goalAssert(long a0, long a1, long a2)
Definition: Native.java:3989
static int goalSize(long a0, long a1)
Definition: Native.java:4023
static void goalIncRef(long a0, long a1)
Definition: Native.java:3964
static String goalToString(long a0, long a1)
Definition: Native.java:4086
static int goalDepth(long a0, long a1)
Definition: Native.java:4006
static long goalFormula(long a0, long a1, int a2)
Definition: Native.java:4032
static long goalConvertModel(long a0, long a1, long a2)
Definition: Native.java:4077
static int goalNumExprs(long a0, long a1)
Definition: Native.java:4041
static long goalTranslate(long a0, long a1, long a2)
Definition: Native.java:4068
static int goalPrecision(long a0, long a1)
Definition: Native.java:3980
static boolean goalIsDecidedUnsat(long a0, long a1)
Definition: Native.java:4059
ApplyResult apply(Goal g)
Definition: Tactic.java:50
static final Z3_goal_prec fromInt(int v)
def String(name, ctx=None)
Definition: z3py.py:10085
def Model(ctx=None)
Definition: z3py.py:6236