41 Contract.Ensures(Contract.Result<
string>() != null);
43 return Native.Z3_tactic_get_help(
Context.nCtx, NativeObject);
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);
110 : base(ctx, Native.Z3_mk_tactic(ctx.nCtx, name))
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)
124 Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
127 internal override void DecRef(
Context ctx, IntPtr obj)
129 Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
133 internal override void IncRef(IntPtr o)
139 internal override void DecRef(IntPtr o)
IDecRefQueue Tactic_DRQ
Tactic DRQ
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...
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.
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...