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 
124 
139  public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
140  {
141  getContext().checkContextMatch(constraints);
142  getContext().checkContextMatch(ps);
143  if (constraints.length != ps.length) {
144  throw new Z3Exception("Argument size mismatch");
145  }
146 
147  for (int i = 0; i < constraints.length; i++) {
148  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
149  constraints[i].getNativeObject(), ps[i].getNativeObject());
150  }
151  }
152 
166  public void assertAndTrack(BoolExpr constraint, BoolExpr p)
167  {
168  getContext().checkContextMatch(constraint);
169  getContext().checkContextMatch(p);
170 
171  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
172  constraint.getNativeObject(), p.getNativeObject());
173  }
174 
178  public void fromFile(String file)
179  {
180  Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
181  }
182 
186  public void fromString(String str)
187  {
188  Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
189  }
190 
191 
197  public int getNumAssertions()
198  {
199  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
200  return assrts.size();
201  }
202 
209  {
210  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
211  return assrts.ToBoolExprArray();
212  }
213 
221  public Status check(Expr... assumptions)
222  {
223  Z3_lbool r;
224  if (assumptions == null) {
225  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
226  getNativeObject()));
227  } else {
229  .nCtx(), getNativeObject(), assumptions.length, AST
230  .arrayToNative(assumptions)));
231  }
232  switch (r)
233  {
234  case Z3_L_TRUE:
235  return Status.SATISFIABLE;
236  case Z3_L_FALSE:
237  return Status.UNSATISFIABLE;
238  default:
239  return Status.UNKNOWN;
240  }
241  }
242 
250  public Status check()
251  {
252  return check((Expr[]) null);
253  }
254 
264  public Model getModel()
265  {
266  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
267  if (x == 0) {
268  return null;
269  } else {
270  return new Model(getContext(), x);
271  }
272  }
273 
283  public Expr getProof()
284  {
285  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
286  if (x == 0) {
287  return null;
288  } else {
289  return Expr.create(getContext(), x);
290  }
291  }
292 
303  {
304 
305  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
306  return core.ToBoolExprArray();
307  }
308 
314  {
315  return Native.solverGetReasonUnknown(getContext().nCtx(),
316  getNativeObject());
317  }
318 
322  public Solver translate(Context ctx)
323  {
324  return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
325  }
326 
333  {
334  return new Statistics(getContext(), Native.solverGetStatistics(
335  getContext().nCtx(), getNativeObject()));
336  }
337 
341  @Override
342  public String toString()
343  {
344  return Native
345  .solverToString(getContext().nCtx(), getNativeObject());
346  }
347 
348  Solver(Context ctx, long obj)
349  {
350  super(ctx, obj);
351  }
352 
353  @Override
354  void incRef() {
355  Native.solverIncRef(getContext().nCtx(), getNativeObject());
356  }
357 
358  @Override
359  void addToReferenceQueue() {
360  getContext().getSolverDRQ().storeReference(getContext(), this);
361  }
362 }
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.Native.solverSetParams
static void solverSetParams(long a0, long a1, long a2)
Definition: Native.java:4565
com.microsoft.z3.Solver.fromString
void fromString(String str)
Load solver assertions from a string.
Definition: Solver.java:186
com.microsoft.z3.Solver.add
void add(BoolExpr... constraints)
Definition: Solver.java:114
com.microsoft.z3.Context.getSolverDRQ
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4083
com.microsoft.z3.Solver.getNumAssertions
int getNumAssertions()
Definition: Solver.java:197
com.microsoft.z3.Status.SATISFIABLE
SATISFIABLE
Definition: Status.java:32
com.microsoft.z3.Native.solverGetUnsatCore
static long solverGetUnsatCore(long a0, long a1)
Definition: Native.java:4769
com.microsoft.z3.Solver.check
Status check()
Definition: Solver.java:250
com.microsoft.z3.Native.solverAssertAndTrack
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
Definition: Native.java:4638
com.microsoft.z3.Native.solverFromString
static void solverFromString(long a0, long a1, String a2)
Definition: Native.java:4654
com.microsoft.z3.Solver.assertAndTrack
void assertAndTrack(BoolExpr constraint, BoolExpr p)
Definition: Solver.java:166
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.Solver.getStatistics
Statistics getStatistics()
Definition: Solver.java:332
com.microsoft.z3.Native.solverPush
static void solverPush(long a0, long a1)
Definition: Native.java:4597
com.microsoft.z3.enumerations.Z3_lbool.fromInt
static final Z3_lbool fromInt(int v)
Definition: Z3_lbool.java:34
com.microsoft
com.microsoft.z3.Native.solverCheck
static int solverCheck(long a0, long a1)
Definition: Native.java:4706
com.microsoft.z3.ParamDescrs
Definition: ParamDescrs.java:25
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Native.solverGetModel
static long solverGetModel(long a0, long a1)
Definition: Native.java:4751
Z3_L_TRUE
@ Z3_L_TRUE
Definition: z3_api.h:103
com.microsoft.z3.Native.solverGetReasonUnknown
static String solverGetReasonUnknown(long a0, long a1)
Definition: Native.java:4778
com.microsoft.z3.Solver.getParameterDescriptions
ParamDescrs getParameterDescriptions()
Definition: Solver.java:52
com.microsoft.z3.Solver.pop
void pop()
Definition: Solver.java:82
com.microsoft.z3.Solver
Definition: Solver.java:26
com.microsoft.z3.Native.solverCheckAssumptions
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
Definition: Native.java:4715
com.microsoft.z3.Native.solverGetNumScopes
static int solverGetNumScopes(long a0, long a1)
Definition: Native.java:4621
com.microsoft.z3.Solver.getUnsatCore
BoolExpr[] getUnsatCore()
Definition: Solver.java:302
com.microsoft.z3.Native.solverGetHelp
static String solverGetHelp(long a0, long a1)
Definition: Native.java:4547
com.microsoft.z3.ASTVector.size
int size()
Definition: ASTVector.java:27
com.microsoft.z3.Solver.getModel
Model getModel()
Definition: Solver.java:264
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6236
com.microsoft.z3.Model
Definition: Model.java:25
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Solver.getAssertions
BoolExpr[] getAssertions()
Definition: Solver.java:208
com.microsoft.z3.Solver.getReasonUnknown
String getReasonUnknown()
Definition: Solver.java:313
com.microsoft.z3.Native.solverTranslate
static long solverTranslate(long a0, long a1, long a2)
Definition: Native.java:4530
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.solverGetParamDescrs
static long solverGetParamDescrs(long a0, long a1)
Definition: Native.java:4556
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Native.solverPop
static void solverPop(long a0, long a1, int a2)
Definition: Native.java:4605
com.microsoft.z3.Solver.translate
Solver translate(Context ctx)
Definition: Solver.java:322
com.microsoft.z3.Solver.pop
void pop(int n)
Definition: Solver.java:94
com.microsoft.z3.Expr
Definition: Expr.java:30
com.microsoft.z3.Solver.assertAndTrack
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Definition: Solver.java:139
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:25
com.microsoft.z3.AST
Definition: AST.java:25
com.microsoft.z3.enumerations.Z3_lbool
Definition: Z3_lbool.java:13
com.microsoft.z3.Native.solverGetStatistics
static long solverGetStatistics(long a0, long a1)
Definition: Native.java:4787
com.microsoft.z3.Solver.getProof
Expr getProof()
Definition: Solver.java:283
com.microsoft.z3.Solver.check
Status check(Expr... assumptions)
Definition: Solver.java:221
com.microsoft.z3.Native.solverGetAssertions
static long solverGetAssertions(long a0, long a1)
Definition: Native.java:4662
com.microsoft.z3.Status.UNKNOWN
UNKNOWN
Definition: Status.java:29
Z3_L_FALSE
@ Z3_L_FALSE
Definition: z3_api.h:101
com.microsoft.z3.Solver.toString
String toString()
Definition: Solver.java:342
com.microsoft.z3.Native.solverReset
static void solverReset(long a0, long a1)
Definition: Native.java:4613
com.microsoft.z3.Native.solverFromFile
static void solverFromFile(long a0, long a1, String a2)
Definition: Native.java:4646
com.microsoft.z3.Status
Definition: Status.java:23
com.microsoft.z3.Solver.getHelp
String getHelp()
Definition: Solver.java:30
com
com.microsoft.z3.Native.solverToString
static String solverToString(long a0, long a1)
Definition: Native.java:4796
com.microsoft.z3.Native.solverGetProof
static long solverGetProof(long a0, long a1)
Definition: Native.java:4760
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Solver.push
void push()
Definition: Solver.java:73
com.microsoft.z3.Native.solverAssert
static void solverAssert(long a0, long a1, long a2)
Definition: Native.java:4630
com.microsoft.z3.Status.UNSATISFIABLE
UNSATISFIABLE
Definition: Status.java:26
com.microsoft.z3.Solver.setParameters
void setParameters(Params value)
Definition: Solver.java:40
com.microsoft.z3.Statistics
Definition: Statistics.java:23
com.microsoft.z3.Solver.reset
void reset()
Definition: Solver.java:104
com.microsoft.z3.Solver.getNumScopes
int getNumScopes()
Definition: Solver.java:63
com.microsoft.z3.Solver.fromFile
void fromFile(String file)
Load solver assertions from a file.
Definition: Solver.java:178
com.microsoft.z3.ASTVector.ToBoolExprArray
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10085