21using System.Diagnostics;
41 return Native.Z3_tactic_get_help(
Context.nCtx, NativeObject);
60 Debug.Assert(g !=
null);
79 Debug.Assert(g !=
null);
102 Debug.Assert(ctx !=
null);
104 internal Tactic(Context ctx,
string name)
107 Debug.Assert(ctx !=
null);
113 internal class DecRefQueue : IDecRefQueue
115 public DecRefQueue() : base() { }
116 public DecRefQueue(uint move_limit) : base(move_limit) { }
117 internal override void IncRef(Context ctx, IntPtr obj)
119 Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
122 internal override void DecRef(Context ctx, IntPtr obj)
124 Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
128 internal override void IncRef(IntPtr o)
134 internal override void DecRef(IntPtr o)
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
The main interaction with Z3 happens via the Context.
IDecRefQueue Tactic_DRQ
Tactic DRQ
Solver MkSolver(Symbol logic=null)
Creates a new (incremental) solver.
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
A ParamDescrs describes a set of parameters.
A Params objects represents a configuration in the form of Symbol/value pairs.
Tactics are the basic building block for creating custom solvers for specific problem domains....
string Help
A string containing a description of parameters accepted by the tactic.
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Tactics.
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_tactic Z3_API Z3_mk_tactic(Z3_context c, Z3_string name)
Return a tactic associated with the given name. The complete list of tactics may be obtained using th...