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() throws Z3Exception
31  {
32  return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
33  }
34 
40  public void setParameters(Params value) throws Z3Exception
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 
62  public int getNumScopes() throws Z3Exception
63  {
64  return Native
65  .solverGetNumScopes(getContext().nCtx(), getNativeObject());
66  }
67 
71  public void push() throws Z3Exception
72  {
73  Native.solverPush(getContext().nCtx(), getNativeObject());
74  }
75 
79  public void pop() throws Z3Exception
80  {
81  pop(1);
82  }
83 
89  public void pop(int n) throws Z3Exception
90  {
91  Native.solverPop(getContext().nCtx(), getNativeObject(), n);
92  }
93 
98  public void reset() throws Z3Exception
99  {
100  Native.solverReset(getContext().nCtx(), getNativeObject());
101  }
102 
108  public void add(BoolExpr... constraints) throws Z3Exception
109  {
110  getContext().checkContextMatch(constraints);
111  for (BoolExpr a : constraints)
112  {
113  Native.solverAssert(getContext().nCtx(), getNativeObject(),
114  a.getNativeObject());
115  }
116  }
117 
118  // / <summary>
119  // / Assert multiple constraints into the solver, and track them (in the
120  // unsat) core
121  // / using the Boolean constants in ps.
122  // / </summary>
123  // / <remarks>
124  // / This API is an alternative to <see cref="Check"/> with assumptions for
125  // extracting unsat cores.
126  // / Both APIs can be used in the same solver. The unsat core will contain a
127  // combination
128  // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
129  // and the Boolean literals
130  // / provided using <see cref="Check"/> with assumptions.
131  // / </remarks>
132  public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception
133  {
134  getContext().checkContextMatch(constraints);
135  getContext().checkContextMatch(ps);
136  if (constraints.length != ps.length)
137  throw new Z3Exception("Argument size mismatch");
138 
139  for (int i = 0; i < constraints.length; i++)
140  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
141  constraints[i].getNativeObject(), ps[i].getNativeObject());
142  }
143 
144  // / <summary>
145  // / Assert a constraint into the solver, and track it (in the unsat) core
146  // / using the Boolean constant p.
147  // / </summary>
148  // / <remarks>
149  // / This API is an alternative to <see cref="Check"/> with assumptions for
150  // extracting unsat cores.
151  // / Both APIs can be used in the same solver. The unsat core will contain a
152  // combination
153  // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
154  // and the Boolean literals
155  // / provided using <see cref="Check"/> with assumptions.
156  // / </remarks>
157  public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception
158  {
159  getContext().checkContextMatch(constraint);
160  getContext().checkContextMatch(p);
161 
162  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
163  constraint.getNativeObject(), p.getNativeObject());
164  }
165 
171  public int getNumAssertions() throws Z3Exception
172  {
173  ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
174  getContext().nCtx(), getNativeObject()));
175  return ass.size();
176  }
177 
184  {
185  ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
186  getContext().nCtx(), getNativeObject()));
187  int n = ass.size();
188  BoolExpr[] res = new BoolExpr[n];
189  for (int i = 0; i < n; i++)
190  res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject());
191  return res;
192  }
193 
199  public Status check(Expr... assumptions) throws Z3Exception
200  {
201  Z3_lbool r;
202  if (assumptions == null)
203  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
204  getNativeObject()));
205  else
207  .nCtx(), getNativeObject(), (int) assumptions.length, AST
208  .arrayToNative(assumptions)));
209  switch (r)
210  {
211  case Z3_L_TRUE:
212  return Status.SATISFIABLE;
213  case Z3_L_FALSE:
214  return Status.UNSATISFIABLE;
215  default:
216  return Status.UNKNOWN;
217  }
218  }
219 
225  public Status check() throws Z3Exception
226  {
227  return check((Expr[]) null);
228  }
229 
238  public Model getModel() throws Z3Exception
239  {
240  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
241  if (x == 0)
242  return null;
243  else
244  return new Model(getContext(), x);
245  }
246 
255  public Expr getProof() throws Z3Exception
256  {
257  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
258  if (x == 0)
259  return null;
260  else
261  return Expr.create(getContext(), x);
262  }
263 
272  public Expr[] getUnsatCore() throws Z3Exception
273  {
274 
275  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
276  getContext().nCtx(), getNativeObject()));
277  int n = core.size();
278  Expr[] res = new Expr[n];
279  for (int i = 0; i < n; i++)
280  res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
281  return res;
282  }
283 
288  public String getReasonUnknown() throws Z3Exception
289  {
290  return Native.solverGetReasonUnknown(getContext().nCtx(),
291  getNativeObject());
292  }
293 
300  {
301  return new Statistics(getContext(), Native.solverGetStatistics(
302  getContext().nCtx(), getNativeObject()));
303  }
304 
308  public String toString()
309  {
310  try
311  {
312  return Native
313  .solverToString(getContext().nCtx(), getNativeObject());
314  } catch (Z3Exception e)
315  {
316  return "Z3Exception: " + e.getMessage();
317  }
318  }
319 
320  Solver(Context ctx, long obj) throws Z3Exception
321  {
322  super(ctx, obj);
323  }
324 
325  void incRef(long o) throws Z3Exception
326  {
327  getContext().solver_DRQ().incAndClear(getContext(), o);
328  super.incRef(o);
329  }
330 
331  void decRef(long o) throws Z3Exception
332  {
333  getContext().solver_DRQ().add(o);
334  super.decRef(o);
335  }
336 }
ParamDescrs getParameterDescriptions()
Definition: Solver.java:52
static String solverGetReasonUnknown(long a0, long a1)
Definition: Native.java:4328
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Definition: Solver.java:132
static long solverGetParamDescrs(long a0, long a1)
Definition: Native.java:4192
static long solverGetStatistics(long a0, long a1)
Definition: Native.java:4337
static void solverReset(long a0, long a1)
Definition: Native.java:4241
void setParameters(Params value)
Definition: Solver.java:40
Status check(Expr...assumptions)
Definition: Solver.java:199
void assertAndTrack(BoolExpr constraint, BoolExpr p)
Definition: Solver.java:157
static long solverGetProof(long a0, long a1)
Definition: Native.java:4310
void add(BoolExpr...constraints)
Definition: Solver.java:108
String getReasonUnknown()
Definition: Solver.java:288
static int solverGetNumScopes(long a0, long a1)
Definition: Native.java:4249
static void solverPush(long a0, long a1)
Definition: Native.java:4225
static void solverAssert(long a0, long a1, long a2)
Definition: Native.java:4258
static String solverGetHelp(long a0, long a1)
Definition: Native.java:4183
static String solverToString(long a0, long a1)
Definition: Native.java:4346
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
Definition: Native.java:4292
static void solverSetParams(long a0, long a1, long a2)
Definition: Native.java:4201
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
Definition: Native.java:4266
static long solverGetModel(long a0, long a1)
Definition: Native.java:4301
Statistics getStatistics()
Definition: Solver.java:299
static long solverGetAssertions(long a0, long a1)
Definition: Native.java:4274
static long solverGetUnsatCore(long a0, long a1)
Definition: Native.java:4319
static int solverCheck(long a0, long a1)
Definition: Native.java:4283
static void solverPop(long a0, long a1, int a2)
Definition: Native.java:4233
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:21
BoolExpr[] getAssertions()
Definition: Solver.java:183