Z3
src/api/java/Solver.java
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     // / <summary>
00119     // / Assert multiple constraints into the solver, and track them (in the
00120     // unsat) core
00121     // / using the Boolean constants in ps.
00122     // / </summary>
00123     // / <remarks>
00124     // / This API is an alternative to <see cref="Check"/> with assumptions for
00125     // extracting unsat cores.
00126     // / Both APIs can be used in the same solver. The unsat core will contain a
00127     // combination
00128     // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
00129     // and the Boolean literals
00130     // / provided using <see cref="Check"/> with assumptions.
00131     // / </remarks>
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     // / <summary>
00145     // / Assert a constraint into the solver, and track it (in the unsat) core
00146     // / using the Boolean constant p.
00147     // / </summary>
00148     // / <remarks>
00149     // / This API is an alternative to <see cref="Check"/> with assumptions for
00150     // extracting unsat cores.
00151     // / Both APIs can be used in the same solver. The unsat core will contain a
00152     // combination
00153     // / of the Boolean variables provided using <see cref="AssertAndTrack"/>
00154     // and the Boolean literals
00155     // / provided using <see cref="Check"/> with assumptions.
00156     // / </remarks>
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines