Z3
Solver.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class Solver extends Z3Object
26 {
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 
138  public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
139  {
140  getContext().checkContextMatch(constraints);
141  getContext().checkContextMatch(ps);
142  if (constraints.length != ps.length)
143  throw new Z3Exception("Argument size mismatch");
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 
163  public void assertAndTrack(BoolExpr constraint, BoolExpr p)
164  {
165  getContext().checkContextMatch(constraint);
166  getContext().checkContextMatch(p);
167 
168  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
169  constraint.getNativeObject(), p.getNativeObject());
170  }
171 
177  public int getNumAssertions()
178  {
179  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
180  getContext().nCtx(), getNativeObject()));
181  return assrts.size();
182  }
183 
190  {
191  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
192  getContext().nCtx(), getNativeObject()));
193  int n = assrts.size();
194  BoolExpr[] res = new BoolExpr[n];
195  for (int i = 0; i < n; i++)
196  res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
197  return res;
198  }
199 
207  public Status check(Expr... assumptions)
208  {
209  Z3_lbool r;
210  if (assumptions == null)
211  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
212  getNativeObject()));
213  else
215  .nCtx(), getNativeObject(), (int) assumptions.length, AST
216  .arrayToNative(assumptions)));
217  switch (r)
218  {
219  case Z3_L_TRUE:
220  return Status.SATISFIABLE;
221  case Z3_L_FALSE:
222  return Status.UNSATISFIABLE;
223  default:
224  return Status.UNKNOWN;
225  }
226  }
227 
235  public Status check()
236  {
237  return check((Expr[]) null);
238  }
239 
249  public Model getModel()
250  {
251  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
252  if (x == 0)
253  return null;
254  else
255  return new Model(getContext(), x);
256  }
257 
267  public Expr getProof()
268  {
269  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
270  if (x == 0)
271  return null;
272  else
273  return Expr.create(getContext(), x);
274  }
275 
285  public Expr[] getUnsatCore()
286  {
287 
288  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
289  getContext().nCtx(), getNativeObject()));
290  int n = core.size();
291  Expr[] res = new Expr[n];
292  for (int i = 0; i < n; i++)
293  res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
294  return res;
295  }
296 
301  public String getReasonUnknown()
302  {
303  return Native.solverGetReasonUnknown(getContext().nCtx(),
304  getNativeObject());
305  }
306 
313  {
314  return new Statistics(getContext(), Native.solverGetStatistics(
315  getContext().nCtx(), getNativeObject()));
316  }
317 
321  public String toString()
322  {
323  try
324  {
325  return Native
326  .solverToString(getContext().nCtx(), getNativeObject());
327  } catch (Z3Exception e)
328  {
329  return "Z3Exception: " + e.getMessage();
330  }
331  }
332 
333  Solver(Context ctx, long obj)
334  {
335  super(ctx, obj);
336  }
337 
338  void incRef(long o)
339  {
340  getContext().getSolverDRQ().incAndClear(getContext(), o);
341  super.incRef(o);
342  }
343 
344  void decRef(long o)
345  {
346  getContext().getSolverDRQ().add(o);
347  super.decRef(o);
348  }
349 }
ParamDescrs getParameterDescriptions()
Definition: Solver.java:52
static String solverGetReasonUnknown(long a0, long a1)
Definition: Native.java:4397
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Definition: Solver.java:138
static long solverGetParamDescrs(long a0, long a1)
Definition: Native.java:4261
static long solverGetStatistics(long a0, long a1)
Definition: Native.java:4406
static void solverReset(long a0, long a1)
Definition: Native.java:4310
void setParameters(Params value)
Definition: Solver.java:40
Status check(Expr...assumptions)
Definition: Solver.java:207
void assertAndTrack(BoolExpr constraint, BoolExpr p)
Definition: Solver.java:163
static long solverGetProof(long a0, long a1)
Definition: Native.java:4379
void add(BoolExpr...constraints)
Definition: Solver.java:114
String getReasonUnknown()
Definition: Solver.java:301
static int solverGetNumScopes(long a0, long a1)
Definition: Native.java:4318
void incAndClear(Context ctx, long o)
static void solverPush(long a0, long a1)
Definition: Native.java:4294
static void solverAssert(long a0, long a1, long a2)
Definition: Native.java:4327
static String solverGetHelp(long a0, long a1)
Definition: Native.java:4252
static String solverToString(long a0, long a1)
Definition: Native.java:4415
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
Definition: Native.java:4361
static void solverSetParams(long a0, long a1, long a2)
Definition: Native.java:4270
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
Definition: Native.java:4335
IDecRefQueue getSolverDRQ()
Definition: Context.java:3720
static long solverGetModel(long a0, long a1)
Definition: Native.java:4370
Statistics getStatistics()
Definition: Solver.java:312
static long solverGetAssertions(long a0, long a1)
Definition: Native.java:4343
static long solverGetUnsatCore(long a0, long a1)
Definition: Native.java:4388
static int solverCheck(long a0, long a1)
Definition: Native.java:4352
static void solverPop(long a0, long a1, int a2)
Definition: Native.java:4302
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
BoolExpr[] getAssertions()
Definition: Solver.java:189