Z3
Solver.java
Go to the documentation of this file.
1
19package com.microsoft.z3;
20
21import com.microsoft.z3.enumerations.Z3_lbool;
22
26public class Solver extends Z3Object {
30 public String getHelp()
31 {
32 return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
33 }
34
40 public void setParameters(Params value)
41 {
42 getContext().checkContextMatch(value);
43 Native.solverSetParams(getContext().nCtx(), getNativeObject(),
44 value.getNativeObject());
45 }
46
53 {
54 return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
55 getContext().nCtx(), getNativeObject()));
56 }
57
63 public int getNumScopes()
64 {
65 return Native
66 .solverGetNumScopes(getContext().nCtx(), getNativeObject());
67 }
68
73 public void push()
74 {
75 Native.solverPush(getContext().nCtx(), getNativeObject());
76 }
77
82 public void pop()
83 {
84 pop(1);
85 }
86
94 public void pop(int n)
95 {
96 Native.solverPop(getContext().nCtx(), getNativeObject(), n);
97 }
98
104 public void reset()
105 {
106 Native.solverReset(getContext().nCtx(), getNativeObject());
107 }
108
114 public void add(BoolExpr... constraints)
115 {
116 getContext().checkContextMatch(constraints);
117 for (BoolExpr a : constraints)
118 {
119 Native.solverAssert(getContext().nCtx(), getNativeObject(),
120 a.getNativeObject());
121 }
122 }
123
124
139 public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
140 {
141 getContext().checkContextMatch(constraints);
142 getContext().checkContextMatch(ps);
143 if (constraints.length != ps.length) {
144 throw new Z3Exception("Argument size mismatch");
145 }
146
147 for (int i = 0; i < constraints.length; i++) {
148 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
149 constraints[i].getNativeObject(), ps[i].getNativeObject());
150 }
151 }
152
166 public void assertAndTrack(BoolExpr constraint, BoolExpr p)
167 {
168 getContext().checkContextMatch(constraint);
169 getContext().checkContextMatch(p);
170
171 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
172 constraint.getNativeObject(), p.getNativeObject());
173 }
174
178 public void fromFile(String file)
179 {
180 Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
181 }
182
186 public void fromString(String str)
187 {
188 Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
189 }
190
191
197 public int getNumAssertions()
198 {
199 ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
200 return assrts.size();
201 }
202
209 {
210 ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
211 return assrts.ToBoolExprArray();
212 }
213
221 public Status check(Expr... assumptions)
222 {
223 Z3_lbool r;
224 if (assumptions == null) {
225 r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
226 getNativeObject()));
227 } else {
229 .nCtx(), getNativeObject(), assumptions.length, AST
230 .arrayToNative(assumptions)));
231 }
232 switch (r)
233 {
234 case Z3_L_TRUE:
235 return Status.SATISFIABLE;
236 case Z3_L_FALSE:
237 return Status.UNSATISFIABLE;
238 default:
239 return Status.UNKNOWN;
240 }
241 }
242
250 public Status check()
251 {
252 return check((Expr[]) null);
253 }
254
265 {
266 long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
267 if (x == 0) {
268 return null;
269 } else {
270 return new Model(getContext(), x);
271 }
272 }
273
283 public Expr getProof()
284 {
285 long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
286 if (x == 0) {
287 return null;
288 } else {
289 return Expr.create(getContext(), x);
290 }
291 }
292
303 {
304
305 ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
306 return core.ToBoolExprArray();
307 }
308
314 {
315 return Native.solverGetReasonUnknown(getContext().nCtx(),
316 getNativeObject());
317 }
318
323 {
324 return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
325 }
326
333 {
334 return new Statistics(getContext(), Native.solverGetStatistics(
335 getContext().nCtx(), getNativeObject()));
336 }
337
341 @Override
343 {
344 return Native
345 .solverToString(getContext().nCtx(), getNativeObject());
346 }
347
348 Solver(Context ctx, long obj)
349 {
350 super(ctx, obj);
351 }
352
353 @Override
354 void incRef() {
355 Native.solverIncRef(getContext().nCtx(), getNativeObject());
356 }
357
358 @Override
359 void addToReferenceQueue() {
360 getContext().getSolverDRQ().storeReference(getContext(), this);
361 }
362}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4083
void storeReference(Context ctx, T obj)
static long solverGetModel(long a0, long a1)
Definition: Native.java:4751
static int solverCheck(long a0, long a1)
Definition: Native.java:4706
static void solverFromString(long a0, long a1, String a2)
Definition: Native.java:4654
static long solverGetParamDescrs(long a0, long a1)
Definition: Native.java:4556
static void solverFromFile(long a0, long a1, String a2)
Definition: Native.java:4646
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
Definition: Native.java:4715
static long solverGetAssertions(long a0, long a1)
Definition: Native.java:4662
static String solverGetHelp(long a0, long a1)
Definition: Native.java:4547
static void solverPush(long a0, long a1)
Definition: Native.java:4597
static String solverToString(long a0, long a1)
Definition: Native.java:4796
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
Definition: Native.java:4638
static String solverGetReasonUnknown(long a0, long a1)
Definition: Native.java:4778
static long solverTranslate(long a0, long a1, long a2)
Definition: Native.java:4530
static int solverGetNumScopes(long a0, long a1)
Definition: Native.java:4621
static long solverGetUnsatCore(long a0, long a1)
Definition: Native.java:4769
static void solverAssert(long a0, long a1, long a2)
Definition: Native.java:4630
static void solverSetParams(long a0, long a1, long a2)
Definition: Native.java:4565
static long solverGetProof(long a0, long a1)
Definition: Native.java:4760
static void solverPop(long a0, long a1, int a2)
Definition: Native.java:4605
static void solverReset(long a0, long a1)
Definition: Native.java:4613
static long solverGetStatistics(long a0, long a1)
Definition: Native.java:4787
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Definition: Solver.java:139
Solver translate(Context ctx)
Definition: Solver.java:322
ParamDescrs getParameterDescriptions()
Definition: Solver.java:52
void add(BoolExpr... constraints)
Definition: Solver.java:114
void assertAndTrack(BoolExpr constraint, BoolExpr p)
Definition: Solver.java:166
void setParameters(Params value)
Definition: Solver.java:40
BoolExpr[] getUnsatCore()
Definition: Solver.java:302
Status check(Expr... assumptions)
Definition: Solver.java:221
BoolExpr[] getAssertions()
Definition: Solver.java:208
void fromString(String str)
Load solver assertions from a string.
Definition: Solver.java:186
void fromFile(String file)
Load solver assertions from a file.
Definition: Solver.java:178
String getReasonUnknown()
Definition: Solver.java:313
Statistics getStatistics()
Definition: Solver.java:332
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
def String(name, ctx=None)
Definition: z3py.py:10085
def Model(ctx=None)
Definition: z3py.py:6236
@ Z3_L_TRUE
Definition: z3_api.h:103
@ Z3_L_FALSE
Definition: z3_api.h:101