Z3
Solver.java
Go to the documentation of this file.
1 
19 package com.microsoft.z3;
20 
22 
26 public class Solver extends Z3Object {
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 
127  public void fromFile(String file)
128  {
129  Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
130  }
131 
135  public void fromString(String str)
136  {
137  Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
138  }
139 
140 
155  public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
156  {
157  getContext().checkContextMatch(constraints);
158  getContext().checkContextMatch(ps);
159  if (constraints.length != ps.length) {
160  throw new Z3Exception("Argument size mismatch");
161  }
162 
163  for (int i = 0; i < constraints.length; i++) {
164  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
165  constraints[i].getNativeObject(), ps[i].getNativeObject());
166  }
167  }
168 
182  public void assertAndTrack(BoolExpr constraint, BoolExpr p)
183  {
184  getContext().checkContextMatch(constraint);
185  getContext().checkContextMatch(p);
186 
187  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
188  constraint.getNativeObject(), p.getNativeObject());
189  }
190 
196  public int getNumAssertions()
197  {
198  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
199  return assrts.size();
200  }
201 
208  {
209  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
210  return assrts.ToBoolExprArray();
211  }
212 
220  public Status check(Expr... assumptions)
221  {
222  Z3_lbool r;
223  if (assumptions == null) {
224  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
225  getNativeObject()));
226  } else {
228  .nCtx(), getNativeObject(), assumptions.length, AST
229  .arrayToNative(assumptions)));
230  }
231  switch (r)
232  {
233  case Z3_L_TRUE:
234  return Status.SATISFIABLE;
235  case Z3_L_FALSE:
236  return Status.UNSATISFIABLE;
237  default:
238  return Status.UNKNOWN;
239  }
240  }
241 
249  public Status check()
250  {
251  return check((Expr[]) null);
252  }
253 
263  public Model getModel()
264  {
265  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
266  if (x == 0) {
267  return null;
268  } else {
269  return new Model(getContext(), x);
270  }
271  }
272 
282  public Expr getProof()
283  {
284  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
285  if (x == 0) {
286  return null;
287  } else {
288  return Expr.create(getContext(), x);
289  }
290  }
291 
302  {
303 
304  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
305  return core.ToBoolExprArray();
306  }
307 
313  {
314  return Native.solverGetReasonUnknown(getContext().nCtx(),
315  getNativeObject());
316  }
317 
321  public Solver translate(Context ctx)
322  {
323  return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
324  }
325 
332  {
333  return new Statistics(getContext(), Native.solverGetStatistics(
334  getContext().nCtx(), getNativeObject()));
335  }
336 
340  @Override
341  public String toString()
342  {
343  return Native
344  .solverToString(getContext().nCtx(), getNativeObject());
345  }
346 
347  Solver(Context ctx, long obj)
348  {
349  super(ctx, obj);
350  }
351 
352  @Override
353  void incRef() {
354  Native.solverIncRef(getContext().nCtx(), getNativeObject());
355  }
356 
357  @Override
358  void addToReferenceQueue() {
359  getContext().getSolverDRQ().storeReference(getContext(), this);
360  }
361 }
ParamDescrs getParameterDescriptions()
Definition: Solver.java:52
static String solverGetReasonUnknown(long a0, long a1)
Definition: Native.java:4499
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Definition: Solver.java:155
Solver translate(Context ctx)
Definition: Solver.java:321
static long solverGetParamDescrs(long a0, long a1)
Definition: Native.java:4329
static long solverGetStatistics(long a0, long a1)
Definition: Native.java:4508
static void solverReset(long a0, long a1)
Definition: Native.java:4378
void setParameters(Params value)
Definition: Solver.java:40
static void solverFromString(long a0, long a1, String a2)
Definition: Native.java:4428
void assertAndTrack(BoolExpr constraint, BoolExpr p)
Definition: Solver.java:182
static long solverGetProof(long a0, long a1)
Definition: Native.java:4481
static void solverIncRef(long a0, long a1)
Definition: Native.java:4346
BoolExpr [] ToBoolExprArray()
Definition: ASTVector.java:140
static long solverTranslate(long a0, long a1, long a2)
Definition: Native.java:4311
void storeReference(Context ctx, T obj)
String getReasonUnknown()
Definition: Solver.java:312
static int solverGetNumScopes(long a0, long a1)
Definition: Native.java:4386
void fromString(String str)
Definition: Solver.java:135
static void solverPush(long a0, long a1)
Definition: Native.java:4362
static void solverAssert(long a0, long a1, long a2)
Definition: Native.java:4395
static String solverGetHelp(long a0, long a1)
Definition: Native.java:4320
static String solverToString(long a0, long a1)
Definition: Native.java:4517
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
Definition: Native.java:4445
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4012
Status check(Expr... assumptions)
Definition: Solver.java:220
static void solverSetParams(long a0, long a1, long a2)
Definition: Native.java:4338
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
Definition: Native.java:4403
void add(BoolExpr... constraints)
Definition: Solver.java:114
void fromFile(String file)
Definition: Solver.java:127
BoolExpr [] getUnsatCore()
Definition: Solver.java:301
static long solverGetModel(long a0, long a1)
Definition: Native.java:4472
Statistics getStatistics()
Definition: Solver.java:331
static long solverGetAssertions(long a0, long a1)
Definition: Native.java:4411
static long solverGetUnsatCore(long a0, long a1)
Definition: Native.java:4490
static int solverCheck(long a0, long a1)
Definition: Native.java:4436
static void solverPop(long a0, long a1, int a2)
Definition: Native.java:4370
static void solverFromFile(long a0, long a1, String a2)
Definition: Native.java:4420
def String(name, ctx=None)
Definition: z3py.py:9821
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
BoolExpr [] getAssertions()
Definition: Solver.java:207