Z3
Solver.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class Solver extends Z3Object {
29  public String getHelp()
30  {
31  return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
32  }
33 
39  public void setParameters(Params value)
40  {
41  getContext().checkContextMatch(value);
42  Native.solverSetParams(getContext().nCtx(), getNativeObject(),
43  value.getNativeObject());
44  }
45 
52  {
53  return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
54  getContext().nCtx(), getNativeObject()));
55  }
56 
62  public int getNumScopes()
63  {
64  return Native
65  .solverGetNumScopes(getContext().nCtx(), getNativeObject());
66  }
67 
72  public void push()
73  {
74  Native.solverPush(getContext().nCtx(), getNativeObject());
75  }
76 
81  public void pop()
82  {
83  pop(1);
84  }
85 
93  public void pop(int n)
94  {
95  Native.solverPop(getContext().nCtx(), getNativeObject(), n);
96  }
97 
103  public void reset()
104  {
105  Native.solverReset(getContext().nCtx(), getNativeObject());
106  }
107 
113  public void add(BoolExpr... constraints)
114  {
115  getContext().checkContextMatch(constraints);
116  for (BoolExpr a : constraints)
117  {
118  Native.solverAssert(getContext().nCtx(), getNativeObject(),
119  a.getNativeObject());
120  }
121  }
122 
137  public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
138  {
139  getContext().checkContextMatch(constraints);
140  getContext().checkContextMatch(ps);
141  if (constraints.length != ps.length) {
142  throw new Z3Exception("Argument size mismatch");
143  }
144 
145  for (int i = 0; i < constraints.length; i++) {
146  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
147  constraints[i].getNativeObject(), ps[i].getNativeObject());
148  }
149  }
150 
164  public void assertAndTrack(BoolExpr constraint, BoolExpr p)
165  {
166  getContext().checkContextMatch(constraint);
167  getContext().checkContextMatch(p);
168 
169  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
170  constraint.getNativeObject(), p.getNativeObject());
171  }
172 
178  public int getNumAssertions()
179  {
180  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
181  return assrts.size();
182  }
183 
190  {
191  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
192  return assrts.ToBoolExprArray();
193  }
194 
202  public Status check(Expr... assumptions)
203  {
204  Z3_lbool r;
205  if (assumptions == null) {
206  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
207  getNativeObject()));
208  } else {
210  .nCtx(), getNativeObject(), assumptions.length, AST
211  .arrayToNative(assumptions)));
212  }
213  switch (r)
214  {
215  case Z3_L_TRUE:
216  return Status.SATISFIABLE;
217  case Z3_L_FALSE:
218  return Status.UNSATISFIABLE;
219  default:
220  return Status.UNKNOWN;
221  }
222  }
223 
231  public Status check()
232  {
233  return check((Expr[]) null);
234  }
235 
245  public Model getModel()
246  {
247  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
248  if (x == 0) {
249  return null;
250  } else {
251  return new Model(getContext(), x);
252  }
253  }
254 
264  public Expr getProof()
265  {
266  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
267  if (x == 0) {
268  return null;
269  } else {
270  return Expr.create(getContext(), x);
271  }
272  }
273 
284  {
285 
286  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
287  return core.ToBoolExprArray();
288  }
289 
295  {
296  return Native.solverGetReasonUnknown(getContext().nCtx(),
297  getNativeObject());
298  }
299 
303  public Solver translate(Context ctx)
304  {
305  return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
306  }
307 
314  {
315  return new Statistics(getContext(), Native.solverGetStatistics(
316  getContext().nCtx(), getNativeObject()));
317  }
318 
322  @Override
323  public String toString()
324  {
325  return Native
326  .solverToString(getContext().nCtx(), getNativeObject());
327  }
328 
329  Solver(Context ctx, long obj)
330  {
331  super(ctx, obj);
332  }
333 
334  @Override
335  void incRef() {
336  Native.solverIncRef(getContext().nCtx(), getNativeObject());
337  }
338 
339  @Override
340  void addToReferenceQueue() {
341  getContext().getSolverDRQ().storeReference(getContext(), this);
342  }
343 }
ParamDescrs getParameterDescriptions()
Definition: Solver.java:51
static String solverGetReasonUnknown(long a0, long a1)
Definition: Native.java:4340
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Definition: Solver.java:137
Solver translate(Context ctx)
Definition: Solver.java:303
static long solverGetParamDescrs(long a0, long a1)
Definition: Native.java:4186
static long solverGetStatistics(long a0, long a1)
Definition: Native.java:4349
static void solverReset(long a0, long a1)
Definition: Native.java:4235
void setParameters(Params value)
Definition: Solver.java:39
void assertAndTrack(BoolExpr constraint, BoolExpr p)
Definition: Solver.java:164
static long solverGetProof(long a0, long a1)
Definition: Native.java:4322
static void solverIncRef(long a0, long a1)
Definition: Native.java:4203
BoolExpr [] ToBoolExprArray()
Definition: ASTVector.java:140
static long solverTranslate(long a0, long a1, long a2)
Definition: Native.java:4168
void storeReference(Context ctx, T obj)
String getReasonUnknown()
Definition: Solver.java:294
static int solverGetNumScopes(long a0, long a1)
Definition: Native.java:4243
static void solverPush(long a0, long a1)
Definition: Native.java:4219
static void solverAssert(long a0, long a1, long a2)
Definition: Native.java:4252
static String solverGetHelp(long a0, long a1)
Definition: Native.java:4177
static String solverToString(long a0, long a1)
Definition: Native.java:4358
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
Definition: Native.java:4286
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:3989
Status check(Expr... assumptions)
Definition: Solver.java:202
static void solverSetParams(long a0, long a1, long a2)
Definition: Native.java:4195
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
Definition: Native.java:4260
void add(BoolExpr... constraints)
Definition: Solver.java:113
BoolExpr [] getUnsatCore()
Definition: Solver.java:283
static long solverGetModel(long a0, long a1)
Definition: Native.java:4313
Statistics getStatistics()
Definition: Solver.java:313
static long solverGetAssertions(long a0, long a1)
Definition: Native.java:4268
static long solverGetUnsatCore(long a0, long a1)
Definition: Native.java:4331
static int solverCheck(long a0, long a1)
Definition: Native.java:4277
static void solverPop(long a0, long a1, int a2)
Definition: Native.java:4227
def String(name, ctx=None)
Definition: z3py.py:9443
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
BoolExpr [] getAssertions()
Definition: Solver.java:189