Z3
Solver.java
Go to the documentation of this file.
1 
19 package com.microsoft.z3;
20 
22 import java.util.*;
23 
27 public class Solver extends Z3Object {
31  public String getHelp()
32  {
33  return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
34  }
35 
41  public void setParameters(Params value)
42  {
43  getContext().checkContextMatch(value);
44  Native.solverSetParams(getContext().nCtx(), getNativeObject(),
45  value.getNativeObject());
46  }
47 
54  {
55  return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
56  getContext().nCtx(), getNativeObject()));
57  }
58 
64  public int getNumScopes()
65  {
66  return Native
67  .solverGetNumScopes(getContext().nCtx(), getNativeObject());
68  }
69 
74  public void push()
75  {
76  Native.solverPush(getContext().nCtx(), getNativeObject());
77  }
78 
83  public void pop()
84  {
85  pop(1);
86  }
87 
95  public void pop(int n)
96  {
97  Native.solverPop(getContext().nCtx(), getNativeObject(), n);
98  }
99 
105  public void reset()
106  {
107  Native.solverReset(getContext().nCtx(), getNativeObject());
108  }
109 
115  public void interrupt()
116  {
117  Native.solverInterrupt(getContext().nCtx(), getNativeObject());
118  }
119 
125  public void add(BoolExpr... constraints)
126  {
127  getContext().checkContextMatch(constraints);
128  for (BoolExpr a : constraints)
129  {
130  Native.solverAssert(getContext().nCtx(), getNativeObject(),
131  a.getNativeObject());
132  }
133  }
134 
135 
150  public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
151  {
152  getContext().checkContextMatch(constraints);
153  getContext().checkContextMatch(ps);
154  if (constraints.length != ps.length) {
155  throw new Z3Exception("Argument size mismatch");
156  }
157 
158  for (int i = 0; i < constraints.length; i++) {
159  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
160  constraints[i].getNativeObject(), ps[i].getNativeObject());
161  }
162  }
163 
177  public void assertAndTrack(BoolExpr constraint, BoolExpr p)
178  {
179  getContext().checkContextMatch(constraint);
180  getContext().checkContextMatch(p);
181 
182  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
183  constraint.getNativeObject(), p.getNativeObject());
184  }
185 
189  public void fromFile(String file)
190  {
191  Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
192  }
193 
197  public void fromString(String str)
198  {
199  Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
200  }
201 
202 
208  public int getNumAssertions()
209  {
210  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
211  return assrts.size();
212  }
213 
220  {
221  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
222  return assrts.ToBoolExprArray();
223  }
224 
232  public Status check(Expr... assumptions)
233  {
234  Z3_lbool r;
235  if (assumptions == null) {
236  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
237  getNativeObject()));
238  } else {
240  .nCtx(), getNativeObject(), assumptions.length, AST
241  .arrayToNative(assumptions)));
242  }
243  return lboolToStatus(r);
244  }
245 
253  public Status check()
254  {
255  return check((Expr[]) null);
256  }
257 
269  public Status getConsequences(BoolExpr[] assumptions, Expr[] variables, List<BoolExpr> consequences)
270  {
271  ASTVector result = new ASTVector(getContext());
272  ASTVector asms = new ASTVector(getContext());
273  ASTVector vars = new ASTVector(getContext());
274  for (BoolExpr asm : assumptions) asms.push(asm);
275  for (Expr v : variables) vars.push(v);
276  int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
277  for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject()));
278  return lboolToStatus(Z3_lbool.fromInt(r));
279  }
280 
281 
291  public Model getModel()
292  {
293  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
294  if (x == 0) {
295  return null;
296  } else {
297  return new Model(getContext(), x);
298  }
299  }
300 
310  public Expr getProof()
311  {
312  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
313  if (x == 0) {
314  return null;
315  } else {
316  return Expr.create(getContext(), x);
317  }
318  }
319 
330  {
331 
332  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
333  return core.ToBoolExprArray();
334  }
335 
341  {
342  return Native.solverGetReasonUnknown(getContext().nCtx(),
343  getNativeObject());
344  }
345 
349  public Solver translate(Context ctx)
350  {
351  return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
352  }
353 
360  {
361  return new Statistics(getContext(), Native.solverGetStatistics(
362  getContext().nCtx(), getNativeObject()));
363  }
364 
368  @Override
369  public String toString()
370  {
371  return Native
372  .solverToString(getContext().nCtx(), getNativeObject());
373  }
374 
378  private Status lboolToStatus(Z3_lbool r)
379  {
380  switch (r)
381  {
382  case Z3_L_TRUE:
383  return Status.SATISFIABLE;
384  case Z3_L_FALSE:
385  return Status.UNSATISFIABLE;
386  default:
387  return Status.UNKNOWN;
388  }
389  }
390 
391  Solver(Context ctx, long obj)
392  {
393  super(ctx, obj);
394  }
395 
396  @Override
397  void incRef() {
398  Native.solverIncRef(getContext().nCtx(), getNativeObject());
399  }
400 
401  @Override
402  void addToReferenceQueue() {
403  getContext().getSolverDRQ().storeReference(getContext(), this);
404  }
405 }
com.microsoft.z3.Native.solverInterrupt
static void solverInterrupt(long a0, long a1)
Definition: Native.java:4591
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:4567
com.microsoft.z3.Solver.fromString
void fromString(String str)
Load solver assertions from a string.
Definition: Solver.java:197
com.microsoft.z3.Solver.add
void add(BoolExpr... constraints)
Definition: Solver.java:125
com.microsoft.z3.Context.getSolverDRQ
IDecRefQueue< Solver > getSolverDRQ()
Definition: Context.java:4083
com.microsoft.z3.Solver.getNumAssertions
int getNumAssertions()
Definition: Solver.java:208
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:4771
com.microsoft.z3.Solver.check
Status check()
Definition: Solver.java:253
com.microsoft.z3.Native.solverAssertAndTrack
static void solverAssertAndTrack(long a0, long a1, long a2, long a3)
Definition: Native.java:4640
com.microsoft.z3.Native.solverFromString
static void solverFromString(long a0, long a1, String a2)
Definition: Native.java:4656
com.microsoft.z3.Solver.assertAndTrack
void assertAndTrack(BoolExpr constraint, BoolExpr p)
Definition: Solver.java:177
com.microsoft.z3.ASTVector
Definition: ASTVector.java:23
com.microsoft.z3.Solver.getStatistics
Statistics getStatistics()
Definition: Solver.java:359
com.microsoft.z3.Native.solverPush
static void solverPush(long a0, long a1)
Definition: Native.java:4599
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:4708
com.microsoft.z3.Solver.interrupt
void interrupt()
Definition: Solver.java:115
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:4753
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:4780
com.microsoft.z3.Solver.getParameterDescriptions
ParamDescrs getParameterDescriptions()
Definition: Solver.java:53
com.microsoft.z3.Solver.pop
void pop()
Definition: Solver.java:83
com.microsoft.z3.Solver
Definition: Solver.java:27
com.microsoft.z3.Native.solverCheckAssumptions
static int solverCheckAssumptions(long a0, long a1, int a2, long[] a3)
Definition: Native.java:4717
com.microsoft.z3.Native.solverGetNumScopes
static int solverGetNumScopes(long a0, long a1)
Definition: Native.java:4623
com.microsoft.z3.Solver.getUnsatCore
BoolExpr[] getUnsatCore()
Definition: Solver.java:329
com.microsoft.z3.Native.solverGetHelp
static String solverGetHelp(long a0, long a1)
Definition: Native.java:4549
com.microsoft.z3.ASTVector.size
int size()
Definition: ASTVector.java:27
com.microsoft.z3.Solver.getModel
Model getModel()
Definition: Solver.java:291
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6259
com.microsoft.z3.Model
Definition: Model.java:25
com.microsoft.z3.BoolExpr
Definition: BoolExpr.java:23
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
com.microsoft.z3.Solver.getAssertions
BoolExpr[] getAssertions()
Definition: Solver.java:219
com.microsoft.z3.Solver.getReasonUnknown
String getReasonUnknown()
Definition: Solver.java:340
com.microsoft.z3.Native.solverTranslate
static long solverTranslate(long a0, long a1, long a2)
Definition: Native.java:4532
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.Native.solverGetParamDescrs
static long solverGetParamDescrs(long a0, long a1)
Definition: Native.java:4558
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Native.solverPop
static void solverPop(long a0, long a1, int a2)
Definition: Native.java:4607
com.microsoft.z3.Solver.translate
Solver translate(Context ctx)
Definition: Solver.java:349
com.microsoft.z3.ASTVector.get
AST get(int i)
Definition: ASTVector.java:41
com.microsoft.z3.Solver.getConsequences
Status getConsequences(BoolExpr[] assumptions, Expr[] variables, List< BoolExpr > consequences)
Definition: Solver.java:269
com.microsoft.z3.Solver.pop
void pop(int n)
Definition: Solver.java:95
com.microsoft.z3.Expr
Definition: Expr.java:31
com.microsoft.z3.Solver.assertAndTrack
void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Definition: Solver.java:150
com.microsoft.z3.Z3Exception
Definition: Z3Exception.java:26
com.microsoft.z3.AST
Definition: AST.java:26
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:4789
com.microsoft.z3.Solver.getProof
Expr getProof()
Definition: Solver.java:310
com.microsoft.z3.Solver.check
Status check(Expr... assumptions)
Definition: Solver.java:232
com.microsoft.z3.Native.solverGetAssertions
static long solverGetAssertions(long a0, long a1)
Definition: Native.java:4664
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:369
com.microsoft.z3.Native.solverReset
static void solverReset(long a0, long a1)
Definition: Native.java:4615
com.microsoft.z3.Native.solverFromFile
static void solverFromFile(long a0, long a1, String a2)
Definition: Native.java:4648
com.microsoft.z3.Status
Definition: Status.java:24
com.microsoft.z3.Solver.getHelp
String getHelp()
Definition: Solver.java:31
com
com.microsoft.z3.Native.solverToString
static String solverToString(long a0, long a1)
Definition: Native.java:4798
com.microsoft.z3.Native.solverGetConsequences
static int solverGetConsequences(long a0, long a1, long a2, long a3, long a4)
Definition: Native.java:4735
com.microsoft.z3.Native.solverGetProof
static long solverGetProof(long a0, long a1)
Definition: Native.java:4762
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Solver.push
void push()
Definition: Solver.java:74
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73
com.microsoft.z3.Native.solverAssert
static void solverAssert(long a0, long a1, long a2)
Definition: Native.java:4632
com.microsoft.z3.Status.UNSATISFIABLE
UNSATISFIABLE
Definition: Status.java:26
com.microsoft.z3.Solver.setParameters
void setParameters(Params value)
Definition: Solver.java:41
com.microsoft.z3.Statistics
Definition: Statistics.java:23
com.microsoft.z3.Solver.reset
void reset()
Definition: Solver.java:105
com.microsoft.z3.Solver.getNumScopes
int getNumScopes()
Definition: Solver.java:64
com.microsoft.z3.Solver.fromFile
void fromFile(String file)
Load solver assertions from a file.
Definition: Solver.java:189
com.microsoft.z3.ASTVector.ToBoolExprArray
BoolExpr[] ToBoolExprArray()
Definition: ASTVector.java:140
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
com.microsoft.z3.ASTVector.push
void push(AST a)
Definition: ASTVector.java:68
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111