21 using System.Diagnostics.Contracts;
31 [ContractVerification(
true)]
41 Contract.Ensures(Contract.Result<
string>() != null);
51 public ParamDescrs ParameterDescriptions
62 Contract.Requires(g != null);
63 Contract.Ensures(Contract.Result<
ApplyResult>() != null);
82 Contract.Requires(g != null);
83 Contract.Ensures(Contract.Result<
ApplyResult>() != null);
97 Contract.Ensures(Contract.Result<
Solver>() != null);
107 Contract.Requires(ctx != null);
109 internal Tactic(Context ctx,
string name)
112 Contract.Requires(ctx != null);
117 public override void IncRef(Context ctx, IntPtr obj)
119 Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
122 public override void DecRef(Context ctx, IntPtr obj)
124 Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
128 internal override void IncRef(IntPtr o)
130 Context.Tactic_DRQ.IncAndClear(Context, o);
134 internal override void DecRef(IntPtr o)
136 Context.Tactic_DRQ.Add(o);
Z3_tactic Z3_API Z3_mk_tactic(__in Z3_context c, __in Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...
static Z3_apply_result Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2)
static string Z3_tactic_get_help(Z3_context a0, Z3_tactic a1)
Tactics are the basic building block for creating custom solvers for specific problem domains...
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
static Z3_apply_result Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3)
A ParameterSet represents a configuration in the form of Symbol/value pairs.
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
The main interaction with Z3 happens via the Context.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
static Z3_param_descrs Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1)
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...