Z3 |

Solver.java
Go to the documentation of this file.
1
19 package com.microsoft.z3;
20
21 import com.microsoft.z3.enumerations.Z3_lbool;
22 import 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
54 public ParamDescrs getParameterDescriptions()
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
178 public void assertAndTrack(Expr<BoolSort> constraint, Expr<BoolSort> p)
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
220 public BoolExpr[] getAssertions()
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
294 public Model getModel()
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
313 public Expr<?> getProof()
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
332 public BoolExpr[] getUnsatCore()
333 {
334
335 ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
336 return core.ToBoolExprArray();
337 }
338
343 public String getReasonUnknown()
344 {
345 return Native.solverGetReasonUnknown(getContext().nCtx(),
346 getNativeObject());
347 }
348
352 public Solver translate(Context ctx)
353 {
354 return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
355 }
356
362 public Statistics getStatistics()
363 {
364 return new Statistics(getContext(), Native.solverGetStatistics(
365 getContext().nCtx(), getNativeObject()));
366 }
367
371 @Override
372 public String toString()
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}
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.ASTVector.push
void push(AST a)
Definition: ASTVector.java:68
com.microsoft.z3.ASTVector.get
AST get(int i)
Definition: ASTVector.java:41
com.microsoft.z3.ASTVector.ToBoolExprArray
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
com.microsoft.z3.ASTVector.size
int size()
Definition: ASTVector.java:27
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.Expr< BoolSort >
com.microsoft.z3.Model
Definition: Model.java:26
com.microsoft.z3.ParamDescrs
Definition: ParamDescrs.java:25
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.Solver
Definition: Solver.java:28
com.microsoft.z3.Solver.translate
Solver translate(Context ctx)
Definition: Solver.java:352
com.microsoft.z3.Solver.pop
void pop()
Definition: Solver.java:84
com.microsoft.z3.Solver.getConsequences
Status getConsequences(Expr< BoolSort >[] assumptions, Expr<?>[] variables, List< Expr< BoolSort > > consequences)
Definition: Solver.java:272
com.microsoft.z3.Solver.getParameterDescriptions
ParamDescrs getParameterDescriptions()
Definition: Solver.java:54
com.microsoft.z3.Solver.getProof
Expr<?> getProof()
Definition: Solver.java:313
com.microsoft.z3.Solver.check
final Status check(Expr< BoolSort >... assumptions)
Definition: Solver.java:234
com.microsoft.z3.Solver.assertAndTrack
void assertAndTrack(Expr< BoolSort > constraint, Expr< BoolSort > p)
Definition: Solver.java:178
com.microsoft.z3.Solver.pop
void pop(int n)
Definition: Solver.java:96
com.microsoft.z3.Solver.setParameters
void setParameters(Params value)
Definition: Solver.java:42
com.microsoft.z3.Solver.getUnsatCore
BoolExpr[] getUnsatCore()
Definition: Solver.java:332
com.microsoft.z3.Solver.getHelp
String getHelp()
Definition: Solver.java:32
com.microsoft.z3.Solver.getModel
Model getModel()
Definition: Solver.java:294
com.microsoft.z3.Solver.push
void push()
Definition: Solver.java:75
com.microsoft.z3.Solver.getAssertions
BoolExpr[] getAssertions()
Definition: Solver.java:220
com.microsoft.z3.Solver.getNumScopes
int getNumScopes()
Definition: Solver.java:65
com.microsoft.z3.Solver.fromString
void fromString(String str)
Load solver assertions from a string.
Definition: Solver.java:198
com.microsoft.z3.Solver.toString
String toString()
Definition: Solver.java:372
com.microsoft.z3.Solver.reset
void reset()
Definition: Solver.java:106
com.microsoft.z3.Solver.getNumAssertions
int getNumAssertions()
Definition: Solver.java:209
com.microsoft.z3.Solver.add
void add(Expr< BoolSort >... constraints)
Definition: Solver.java:126
com.microsoft.z3.Solver.fromFile
void fromFile(String file)
Load solver assertions from a file.
Definition: Solver.java:190
com.microsoft.z3.Solver.getReasonUnknown
String getReasonUnknown()
Definition: Solver.java:343
com.microsoft.z3.Solver.interrupt
void interrupt()
Definition: Solver.java:116
com.microsoft.z3.Solver.assertAndTrack
void assertAndTrack(Expr< BoolSort >[] constraints, Expr< BoolSort >[] ps)
Definition: Solver.java:151
com.microsoft.z3.Solver.getStatistics
Statistics getStatistics()
Definition: Solver.java:362
com.microsoft.z3.Statistics
Definition: Statistics.java:23
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.Status
Definition: Status.java:24
com.microsoft.z3.Status.SATISFIABLE
SATISFIABLE
Definition: Status.java:32
com.microsoft.z3.Status.UNSATISFIABLE
UNSATISFIABLE
Definition: Status.java:26
com.microsoft.z3.Status.UNKNOWN
UNKNOWN
Definition: Status.java:29
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:105
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:103