Z3
src/api/dotnet/Solver.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Solver.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Solvers
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-22
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines