00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00028 [ContractVerification(true)]
00029 public class Solver : Z3Object
00030 {
00034 public string Help
00035 {
00036 get
00037 {
00038 Contract.Ensures(Contract.Result<string>() != null);
00039
00040 return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
00041 }
00042 }
00043
00047 public Params Parameters
00048 {
00049 set
00050 {
00051 Contract.Requires(value != null);
00052
00053 Context.CheckContextMatch(value);
00054 Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject);
00055 }
00056 }
00057
00061 public ParamDescrs ParameterDescriptions
00062 {
00063 get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
00064 }
00065
00066
00072 public uint NumScopes
00073 {
00074 get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
00075 }
00076
00081 public void Push()
00082 {
00083 Native.Z3_solver_push(Context.nCtx, NativeObject);
00084 }
00085
00091 public void Pop(uint n = 1)
00092 {
00093 Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
00094 }
00095
00100 public void Reset()
00101 {
00102 Native.Z3_solver_reset(Context.nCtx, NativeObject);
00103 }
00104
00108 public void Assert(params BoolExpr[] constraints)
00109 {
00110 Contract.Requires(constraints != null);
00111 Contract.Requires(Contract.ForAll(constraints, c => c != null));
00112
00113 Context.CheckContextMatch(constraints);
00114 foreach (BoolExpr a in constraints)
00115 {
00116 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
00117 }
00118 }
00119
00123 public void Add(params BoolExpr[] constraints)
00124 {
00125 Assert(constraints);
00126 }
00127
00139 public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
00140 {
00141 Contract.Requires(constraints != null);
00142 Contract.Requires(Contract.ForAll(constraints, c => c != null));
00143 Contract.Requires(Contract.ForAll(ps, c => c != null));
00144 Context.CheckContextMatch(constraints);
00145 Context.CheckContextMatch(ps);
00146 if (constraints.Length != ps.Length)
00147 throw new Z3Exception("Argument size mismatch");
00148
00149 for (int i = 0 ; i < constraints.Length; i++)
00150 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
00151 }
00152
00164 public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
00165 {
00166 Contract.Requires(constraint != null);
00167 Contract.Requires(p != null);
00168 Context.CheckContextMatch(constraint);
00169 Context.CheckContextMatch(p);
00170
00171 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
00172 }
00173
00177 public uint NumAssertions
00178 {
00179 get
00180 {
00181 ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
00182 return ass.Size;
00183 }
00184 }
00185
00189 public BoolExpr[] Assertions
00190 {
00191 get
00192 {
00193 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
00194
00195 ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
00196 uint n = ass.Size;
00197 BoolExpr[] res = new BoolExpr[n];
00198 for (uint i = 0; i < n; i++)
00199 res[i] = new BoolExpr(Context, ass[i].NativeObject);
00200 return res;
00201 }
00202 }
00203
00212 public Status Check(params Expr[] assumptions)
00213 {
00214 Z3_lbool r;
00215 if (assumptions == null || assumptions.Length == 0)
00216 r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
00217 else
00218 r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
00219 switch (r)
00220 {
00221 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
00222 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
00223 default: return Status.UNKNOWN;
00224 }
00225 }
00226
00234 public Model Model
00235 {
00236 get
00237 {
00238 IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
00239 if (x == IntPtr.Zero)
00240 return null;
00241 else
00242 return new Model(Context, x);
00243 }
00244 }
00245
00253 public Expr Proof
00254 {
00255 get
00256 {
00257 IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
00258 if (x == IntPtr.Zero)
00259 return null;
00260 else
00261 return Expr.Create(Context, x);
00262 }
00263 }
00264
00273 public Expr[] UnsatCore
00274 {
00275 get
00276 {
00277 Contract.Ensures(Contract.Result<Expr[]>() != null);
00278
00279 ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
00280 uint n = core.Size;
00281 Expr[] res = new Expr[n];
00282 for (uint i = 0; i < n; i++)
00283 res[i] = Expr.Create(Context, core[i].NativeObject);
00284 return res;
00285 }
00286 }
00287
00291 public string ReasonUnknown
00292 {
00293 get
00294 {
00295 Contract.Ensures(Contract.Result<string>() != null);
00296
00297 return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
00298 }
00299 }
00300
00304 public Statistics Statistics
00305 {
00306 get
00307 {
00308 Contract.Ensures(Contract.Result<Statistics>() != null);
00309
00310 return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
00311 }
00312 }
00313
00317 public override string ToString()
00318 {
00319 return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
00320 }
00321
00322 #region Internal
00323 internal Solver(Context ctx, IntPtr obj)
00324 : base(ctx, obj)
00325 {
00326 Contract.Requires(ctx != null);
00327 }
00328
00329 internal class DecRefQueue : IDecRefQueue
00330 {
00331 public override void IncRef(Context ctx, IntPtr obj)
00332 {
00333 Native.Z3_solver_inc_ref(ctx.nCtx, obj);
00334 }
00335
00336 public override void DecRef(Context ctx, IntPtr obj)
00337 {
00338 Native.Z3_solver_dec_ref(ctx.nCtx, obj);
00339 }
00340 };
00341
00342 internal override void IncRef(IntPtr o)
00343 {
00344 Context.Solver_DRQ.IncAndClear(Context, o);
00345 base.IncRef(o);
00346 }
00347
00348 internal override void DecRef(IntPtr o)
00349 {
00350 Context.Solver_DRQ.Add(o);
00351 base.DecRef(o);
00352 }
00353 #endregion
00354 }
00355 }