Z3
src/api/dotnet/Goal.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Goal.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Goal
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-21
00015 
00016 Notes:
00017     
00018 --*/
00019 
00020 using System;
00021 using System.Diagnostics.Contracts;
00022 
00023 namespace Microsoft.Z3
00024 {
00030     [ContractVerification(true)]
00031     public class Goal : Z3Object
00032     {
00041         public Z3_goal_prec Precision
00042         {
00043             get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); }
00044         }
00045 
00049         public bool IsPrecise
00050         {
00051             get { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
00052         }
00056         public bool IsUnderApproximation
00057         {
00058             get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
00059         }
00060 
00064         public bool IsOverApproximation
00065         {
00066             get { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
00067         }
00068 
00072         public bool IsGarbage
00073         {
00074             get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
00075         }
00076 
00080         public void Assert(params BoolExpr[] constraints)
00081         {
00082             Contract.Requires(constraints != null);
00083             Contract.Requires(Contract.ForAll(constraints, c => c != null));
00084 
00085             Context.CheckContextMatch(constraints);
00086             foreach (BoolExpr c in constraints)
00087             {
00088                 Contract.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress
00089                 Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject);
00090             }
00091         }
00092 
00096         public void Add(params BoolExpr[] constraints)
00097         {
00098             Assert(constraints);
00099         }
00100 
00104         public bool Inconsistent
00105         {
00106             get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
00107         }
00108 
00115         public uint Depth
00116         {
00117             get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
00118         }
00119 
00123         public void Reset()
00124         {
00125             Native.Z3_goal_reset(Context.nCtx, NativeObject);
00126         }
00127 
00131         public uint Size
00132         {
00133             get { return Native.Z3_goal_size(Context.nCtx, NativeObject); }
00134         }
00135 
00139         public BoolExpr[] Formulas
00140         {
00141             get
00142             {
00143                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
00144 
00145                 uint n = Size;
00146                 BoolExpr[] res = new BoolExpr[n];
00147                 for (uint i = 0; i < n; i++)
00148                     res[i] = new BoolExpr(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i));
00149                 return res;
00150             }
00151         }
00152 
00156         public uint NumExprs
00157         {
00158             get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
00159         }
00160 
00164         public bool IsDecidedSat
00165         {
00166             get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
00167         }
00168 
00172         public bool IsDecidedUnsat
00173         {
00174             get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
00175         }
00176 
00180         public Goal Translate(Context ctx)
00181         {
00182             Contract.Requires(ctx != null);
00183 
00184             return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
00185         }
00186 
00191         public Goal Simplify(Params p = null)
00192         {
00193             Tactic t = Context.MkTactic("simplify");
00194             ApplyResult res = t.Apply(this, p);
00195 
00196             if (res.NumSubgoals == 0)
00197                 throw new Z3Exception("No subgoals");
00198             else
00199                 return res.Subgoals[0];
00200         }
00201 
00206         public override string ToString()
00207         {
00208             return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
00209         }
00210 
00211         #region Internal
00212         internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
00213 
00214         internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
00215             : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
00216         {
00217             Contract.Requires(ctx != null);
00218         }
00219 
00220         internal class DecRefQueue : IDecRefQueue
00221         {
00222             public override void IncRef(Context ctx, IntPtr obj)
00223             {
00224                 Native.Z3_goal_inc_ref(ctx.nCtx, obj);
00225             }
00226 
00227             public override void DecRef(Context ctx, IntPtr obj)
00228             {
00229                 Native.Z3_goal_dec_ref(ctx.nCtx, obj);
00230             }
00231         };        
00232 
00233         internal override void IncRef(IntPtr o)
00234         {
00235             Context.Goal_DRQ.IncAndClear(Context, o);
00236             base.IncRef(o);
00237         }
00238 
00239         internal override void DecRef(IntPtr o)
00240         {
00241             Context.Goal_DRQ.Add(o);
00242             base.DecRef(o);
00243         }
00244 
00245         #endregion
00246     }
00247 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines