21 using System.Diagnostics.Contracts;
30 [ContractVerification(
true)]
51 get {
return Precision ==
Z3_goal_prec.Z3_GOAL_PRECISE; }
56 public bool IsUnderApproximation
64 public bool IsOverApproximation
74 get {
return Precision ==
Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
82 Contract.Requires(constraints != null);
83 Contract.Requires(Contract.ForAll(constraints, c => c != null));
85 Context.CheckContextMatch(constraints);
88 Contract.Assert(c != null);
104 public bool Inconsistent
143 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
147 for (uint i = 0; i < n; i++)
164 public bool IsDecidedSat
172 public bool IsDecidedUnsat
182 Contract.Requires(ctx != null);
212 internal Goal(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
214 internal Goal(Context ctx,
bool models,
bool unsatCores,
bool proofs)
215 : base(ctx, Native.
Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
217 Contract.Requires(ctx != null);
222 public override void IncRef(Context ctx, IntPtr obj)
224 Native.Z3_goal_inc_ref(ctx.nCtx, obj);
227 public override void DecRef(Context ctx, IntPtr obj)
229 Native.Z3_goal_dec_ref(ctx.nCtx, obj);
233 internal override void IncRef(IntPtr o)
235 Context.Goal_DRQ.IncAndClear(Context, o);
239 internal override void DecRef(IntPtr o)
241 Context.Goal_DRQ.Add(o);
static uint Z3_goal_num_exprs(Z3_context a0, Z3_goal a1)
void Reset()
Erases all formulas from the given goal.
void Add(params BoolExpr[] constraints)
Alias for Assert.
Tactic MkTactic(string name)
Creates a new Tactic.
static uint Z3_goal_depth(Z3_context a0, Z3_goal a1)
static int Z3_goal_inconsistent(Z3_context a0, Z3_goal a1)
Goal[] Subgoals
Retrieves the subgoals from the ApplyResult.
override string ToString()
Goal to string conversion.
static uint Z3_goal_precision(Z3_context a0, Z3_goal a1)
static Z3_ast Z3_goal_formula(Z3_context a0, Z3_goal a1, uint a2)
Tactics are the basic building block for creating custom solvers for specific problem domains...
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
static string Z3_goal_to_string(Z3_context a0, Z3_goal a1)
static int Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1)
static Z3_goal Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2)
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
static uint Z3_goal_size(Z3_context a0, Z3_goal a1)
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
A ParameterSet represents a configuration in the form of Symbol/value pairs.
static void Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2)
The main interaction with Z3 happens via the Context.
static int Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1)
The exception base class for error reporting from Z3
static void Z3_goal_reset(Z3_context a0, Z3_goal a1)
uint NumSubgoals
The number of Subgoals.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Goal Simplify(Params p=null)
Simplifies the goal.
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Z3_goal Z3_API Z3_mk_goal(__in Z3_context c, __in Z3_bool models, __in Z3_bool unsat_cores, __in Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
Goal Translate(Context ctx)
Translates (copies) the Goal to the target Context ctx .