Z3
src/api/dotnet/Tactic.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Tactic.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Tactics
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 {
00031     [ContractVerification(true)]
00032     public class Tactic : Z3Object
00033     {
00037         public string Help
00038         {
00039             get
00040             {
00041                 Contract.Ensures(Contract.Result<string>() != null);
00042 
00043                 return Native.Z3_tactic_get_help(Context.nCtx, NativeObject);
00044             }
00045         }
00046 
00047 
00051         public ParamDescrs ParameterDescriptions
00052         {
00053             get { return new ParamDescrs(Context, Native.Z3_tactic_get_param_descrs(Context.nCtx, NativeObject)); }
00054         }
00055 
00056 
00060         public ApplyResult Apply(Goal g, Params p = null)
00061         {
00062             Contract.Requires(g != null);
00063             Contract.Ensures(Contract.Result<ApplyResult>() != null);
00064 
00065             Context.CheckContextMatch(g);
00066             if (p == null)
00067                 return new ApplyResult(Context, Native.Z3_tactic_apply(Context.nCtx, NativeObject, g.NativeObject));
00068             else
00069             {
00070                 Context.CheckContextMatch(p);
00071                 return new ApplyResult(Context, Native.Z3_tactic_apply_ex(Context.nCtx, NativeObject, g.NativeObject, p.NativeObject));
00072             }
00073         }
00074 
00078         public ApplyResult this[Goal g]
00079         {
00080             get
00081             {
00082                 Contract.Requires(g != null);
00083                 Contract.Ensures(Contract.Result<ApplyResult>() != null);
00084 
00085                 return Apply(g);
00086             }
00087         }
00088 
00093         public Solver Solver
00094         {
00095             get
00096             {
00097                 Contract.Ensures(Contract.Result<Solver>() != null);
00098 
00099                 return Context.MkSolver(this);
00100             }
00101         }
00102 
00103         #region Internal
00104         internal Tactic(Context ctx, IntPtr obj)
00105             : base(ctx, obj)
00106         {
00107             Contract.Requires(ctx != null);
00108         }
00109         internal Tactic(Context ctx, string name)
00110             : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name))
00111         {
00112             Contract.Requires(ctx != null);
00113         }
00114 
00115         internal class DecRefQueue : IDecRefQueue
00116         {
00117             public override void IncRef(Context ctx, IntPtr obj)
00118             {
00119                 Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
00120             }
00121 
00122             public override void DecRef(Context ctx, IntPtr obj)
00123             {
00124                 Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
00125             }
00126         };
00127 
00128         internal override void IncRef(IntPtr o)
00129         {
00130             Context.Tactic_DRQ.IncAndClear(Context, o);
00131             base.IncRef(o);
00132         }
00133 
00134         internal override void DecRef(IntPtr o)
00135         {
00136             Context.Tactic_DRQ.Add(o);
00137             base.DecRef(o);
00138         }
00139         #endregion
00140     }
00141 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines