Go to the documentation of this file.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 {
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 }