21 using System.Diagnostics.Contracts;
31 [ContractVerification(
true)]
41 Contract.Ensures(Contract.Result<
string>() != null);
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);
112 Contract.Requires(ctx != null);
120 public DecRefQueue() : base() { }
121 public DecRefQueue(uint move_limit) : base(move_limit) { }
122 internal override void IncRef(
Context ctx, IntPtr obj)
127 internal override void DecRef(
Context ctx, IntPtr obj)
133 internal override void IncRef(IntPtr o)
139 internal override void DecRef(IntPtr o)
static Z3_apply_result Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2)
IDecRefQueue Tactic_DRQ
Tactic DRQ
static string Z3_tactic_get_help(Z3_context a0, Z3_tactic a1)
static void Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1)
Tactics are the basic building block for creating custom solvers for specific problem domains...
static Z3_tactic Z3_mk_tactic(Z3_context a0, string a1)
static void Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1)
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 Params objects represents a configuration in the form of Symbol/value pairs.
A ParamDescrs describes a set of parameters.
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 ...