Z3
Solver.java
Go to the documentation of this file.
1
19package com.microsoft.z3;
20
21import com.microsoft.z3.enumerations.Z3_lbool;
22import java.util.*;
23
27@SuppressWarnings("unchecked")
28public class Solver extends Z3Object {
32 public String getHelp()
33 {
34 return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
35 }
36
42 public void setParameters(Params value)
43 {
44 getContext().checkContextMatch(value);
45 Native.solverSetParams(getContext().nCtx(), getNativeObject(),
46 value.getNativeObject());
47 }
48
55 {
56 return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
57 getContext().nCtx(), getNativeObject()));
58 }
59
65 public int getNumScopes()
66 {
67 return Native
68 .solverGetNumScopes(getContext().nCtx(), getNativeObject());
69 }
70
75 public void push()
76 {
77 Native.solverPush(getContext().nCtx(), getNativeObject());
78 }
79
84 public void pop()
85 {
86 pop(1);
87 }
88
96 public void pop(int n)
97 {
98 Native.solverPop(getContext().nCtx(), getNativeObject(), n);
99 }
100
106 public void reset()
107 {
108 Native.solverReset(getContext().nCtx(), getNativeObject());
109 }
110
116 public void interrupt()
117 {
118 Native.solverInterrupt(getContext().nCtx(), getNativeObject());
119 }
120
126 public void add(Expr<BoolSort>... constraints)
127 {
128 getContext().checkContextMatch(constraints);
129 for (Expr<BoolSort> a : constraints)
130 {
131 Native.solverAssert(getContext().nCtx(), getNativeObject(),
132 a.getNativeObject());
133 }
134 }
135
136
151 public void assertAndTrack(Expr<BoolSort>[] constraints, Expr<BoolSort>[] ps)
152 {
153 getContext().checkContextMatch(constraints);
154 getContext().checkContextMatch(ps);
155 if (constraints.length != ps.length) {
156 throw new Z3Exception("Argument size mismatch");
157 }
158
159 for (int i = 0; i < constraints.length; i++) {
160 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
161 constraints[i].getNativeObject(), ps[i].getNativeObject());
162 }
163 }
164
179 {
180 getContext().checkContextMatch(constraint);
181 getContext().checkContextMatch(p);
182
183 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
184 constraint.getNativeObject(), p.getNativeObject());
185 }
186
190 public void fromFile(String file)
191 {
192 Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
193 }
194
198 public void fromString(String str)
199 {
200 Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
201 }
202
203
209 public int getNumAssertions()
210 {
211 ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
212 return assrts.size();
213 }
214
221 {
222 ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
223 return assrts.ToBoolExprArray();
224 }
225
233 @SafeVarargs
234 public final Status check(Expr<BoolSort>... assumptions)
235 {
236 Z3_lbool r;
237 if (assumptions == null) {
238 r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
239 getNativeObject()));
240 } else {
241 r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
242 .nCtx(), getNativeObject(), assumptions.length, AST
243 .arrayToNative(assumptions)));
244 }
245 return lboolToStatus(r);
246 }
247
255 @SuppressWarnings("rawtypes")
256 public Status check()
257 {
258 return check((Expr[]) null);
259 }
260
272 public Status getConsequences(Expr<BoolSort>[] assumptions, Expr<?>[] variables, List<Expr<BoolSort>> consequences)
273 {
274 ASTVector result = new ASTVector(getContext());
275 ASTVector asms = new ASTVector(getContext());
276 ASTVector vars = new ASTVector(getContext());
277 for (Expr<BoolSort> asm : assumptions) asms.push(asm);
278 for (Expr<?> v : variables) vars.push(v);
279 int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
280 for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject()));
281 return lboolToStatus(Z3_lbool.fromInt(r));
282 }
283
284
295 {
296 long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
297 if (x == 0) {
298 return null;
299 } else {
300 return new Model(getContext(), x);
301 }
302 }
303
314 {
315 long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
316 if (x == 0) {
317 return null;
318 } else {
319 return Expr.create(getContext(), x);
320 }
321 }
322
333 {
334
335 ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
336 return core.ToBoolExprArray();
337 }
338
344 {
345 return Native.solverGetReasonUnknown(getContext().nCtx(),
346 getNativeObject());
347 }
348
353 {
354 return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
355 }
356
363 {
364 return new Statistics(getContext(), Native.solverGetStatistics(
365 getContext().nCtx(), getNativeObject()));
366 }
367
371 @Override
373 {
374 return Native
375 .solverToString(getContext().nCtx(), getNativeObject());
376 }
377
381 private Status lboolToStatus(Z3_lbool r)
382 {
383 switch (r)
384 {
385 case Z3_L_TRUE:
386 return Status.SATISFIABLE;
387 case Z3_L_FALSE:
388 return Status.UNSATISFIABLE;
389 default:
390 return Status.UNKNOWN;
391 }
392 }
393
394 Solver(Context ctx, long obj)
395 {
396 super(ctx, obj);
397 }
398
399 @Override
400 void incRef() {
401 Native.solverIncRef(getContext().nCtx(), getNativeObject());
402 }
403
404 @Override
405 void addToReferenceQueue() {
406 getContext().getSolverDRQ().storeReference(getContext(), this);
407 }
408}
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
Solver translate(Context ctx)
Definition: Solver.java:352
Status getConsequences(Expr< BoolSort >[] assumptions, Expr<?>[] variables, List< Expr< BoolSort > > consequences)
Definition: Solver.java:272
ParamDescrs getParameterDescriptions()
Definition: Solver.java:54
final Status check(Expr< BoolSort >... assumptions)
Definition: Solver.java:234
void assertAndTrack(Expr< BoolSort > constraint, Expr< BoolSort > p)
Definition: Solver.java:178
void setParameters(Params value)
Definition: Solver.java:42
BoolExpr[] getUnsatCore()
Definition: Solver.java:332
BoolExpr[] getAssertions()
Definition: Solver.java:220
void fromString(String str)
Load solver assertions from a string.
Definition: Solver.java:198
void add(Expr< BoolSort >... constraints)
Definition: Solver.java:126
void fromFile(String file)
Load solver assertions from a file.
Definition: Solver.java:190
String getReasonUnknown()
Definition: Solver.java:343
void assertAndTrack(Expr< BoolSort >[] constraints, Expr< BoolSort >[] ps)
Definition: Solver.java:151
Statistics getStatistics()
Definition: Solver.java:362
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
def String(name, ctx=None)
Definition: z3py.py:10693
def Model(ctx=None)
Definition: z3py.py:6579
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
@ Z3_L_TRUE
Definition: z3_api.h:105
@ Z3_L_FALSE
Definition: z3_api.h:103