Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00020 import com.microsoft.z3.enumerations.Z3_lbool;
00021
00025 public class Solver extends Z3Object
00026 {
00030 public String getHelp() throws Z3Exception
00031 {
00032 return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
00033 }
00034
00040 public void setParameters(Params value) throws Z3Exception
00041 {
00042 getContext().checkContextMatch(value);
00043 Native.solverSetParams(getContext().nCtx(), getNativeObject(),
00044 value.getNativeObject());
00045 }
00046
00052 public ParamDescrs getParameterDescriptions() throws Z3Exception
00053 {
00054 return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
00055 getContext().nCtx(), getNativeObject()));
00056 }
00057
00062 public int getNumScopes() throws Z3Exception
00063 {
00064 return Native
00065 .solverGetNumScopes(getContext().nCtx(), getNativeObject());
00066 }
00067
00071 public void push() throws Z3Exception
00072 {
00073 Native.solverPush(getContext().nCtx(), getNativeObject());
00074 }
00075
00079 public void pop() throws Z3Exception
00080 {
00081 pop(1);
00082 }
00083
00089 public void pop(int n) throws Z3Exception
00090 {
00091 Native.solverPop(getContext().nCtx(), getNativeObject(), n);
00092 }
00093
00098 public void reset() throws Z3Exception
00099 {
00100 Native.solverReset(getContext().nCtx(), getNativeObject());
00101 }
00102
00108 public void add(BoolExpr... constraints) throws Z3Exception
00109 {
00110 getContext().checkContextMatch(constraints);
00111 for (BoolExpr a : constraints)
00112 {
00113 Native.solverAssert(getContext().nCtx(), getNativeObject(),
00114 a.getNativeObject());
00115 }
00116 }
00117
00118
00119
00120
00121
00122
00123
00124
00125
00126
00127
00128
00129
00130
00131
00132 public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception
00133 {
00134 getContext().checkContextMatch(constraints);
00135 getContext().checkContextMatch(ps);
00136 if (constraints.length != ps.length)
00137 throw new Z3Exception("Argument size mismatch");
00138
00139 for (int i = 0; i < constraints.length; i++)
00140 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
00141 constraints[i].getNativeObject(), ps[i].getNativeObject());
00142 }
00143
00144
00145
00146
00147
00148
00149
00150
00151
00152
00153
00154
00155
00156
00157 public void assertAndTrack(BoolExpr constraint, BoolExpr p) throws Z3Exception
00158 {
00159 getContext().checkContextMatch(constraint);
00160 getContext().checkContextMatch(p);
00161
00162 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
00163 constraint.getNativeObject(), p.getNativeObject());
00164 }
00165
00171 public int getNumAssertions() throws Z3Exception
00172 {
00173 ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
00174 getContext().nCtx(), getNativeObject()));
00175 return ass.size();
00176 }
00177
00183 public BoolExpr[] getAssertions() throws Z3Exception
00184 {
00185 ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
00186 getContext().nCtx(), getNativeObject()));
00187 int n = ass.size();
00188 BoolExpr[] res = new BoolExpr[n];
00189 for (int i = 0; i < n; i++)
00190 res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject());
00191 return res;
00192 }
00193
00199 public Status check(Expr... assumptions) throws Z3Exception
00200 {
00201 Z3_lbool r;
00202 if (assumptions == null)
00203 r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
00204 getNativeObject()));
00205 else
00206 r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
00207 .nCtx(), getNativeObject(), (int) assumptions.length, AST
00208 .arrayToNative(assumptions)));
00209 switch (r)
00210 {
00211 case Z3_L_TRUE:
00212 return Status.SATISFIABLE;
00213 case Z3_L_FALSE:
00214 return Status.UNSATISFIABLE;
00215 default:
00216 return Status.UNKNOWN;
00217 }
00218 }
00219
00225 public Status check() throws Z3Exception
00226 {
00227 return check((Expr[]) null);
00228 }
00229
00238 public Model getModel() throws Z3Exception
00239 {
00240 long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
00241 if (x == 0)
00242 return null;
00243 else
00244 return new Model(getContext(), x);
00245 }
00246
00255 public Expr getProof() throws Z3Exception
00256 {
00257 long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
00258 if (x == 0)
00259 return null;
00260 else
00261 return Expr.create(getContext(), x);
00262 }
00263
00272 public Expr[] getUnsatCore() throws Z3Exception
00273 {
00274
00275 ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
00276 getContext().nCtx(), getNativeObject()));
00277 int n = core.size();
00278 Expr[] res = new Expr[n];
00279 for (int i = 0; i < n; i++)
00280 res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
00281 return res;
00282 }
00283
00288 public String getReasonUnknown() throws Z3Exception
00289 {
00290 return Native.solverGetReasonUnknown(getContext().nCtx(),
00291 getNativeObject());
00292 }
00293
00299 public Statistics getStatistics() throws Z3Exception
00300 {
00301 return new Statistics(getContext(), Native.solverGetStatistics(
00302 getContext().nCtx(), getNativeObject()));
00303 }
00304
00308 public String toString()
00309 {
00310 try
00311 {
00312 return Native
00313 .solverToString(getContext().nCtx(), getNativeObject());
00314 } catch (Z3Exception e)
00315 {
00316 return "Z3Exception: " + e.getMessage();
00317 }
00318 }
00319
00320 Solver(Context ctx, long obj) throws Z3Exception
00321 {
00322 super(ctx, obj);
00323 }
00324
00325 void incRef(long o) throws Z3Exception
00326 {
00327 getContext().solver_DRQ().incAndClear(getContext(), o);
00328 super.incRef(o);
00329 }
00330
00331 void decRef(long o) throws Z3Exception
00332 {
00333 getContext().solver_DRQ().add(o);
00334 super.decRef(o);
00335 }
00336 }