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));
88 Contract.Assert(c != null);
89 Native.Z3_goal_assert(
Context.nCtx, NativeObject, c.NativeObject);
104 public bool Inconsistent
106 get {
return Native.Z3_goal_inconsistent(
Context.nCtx, NativeObject) != 0; }
117 get {
return Native.Z3_goal_depth(
Context.nCtx, NativeObject); }
125 Native.Z3_goal_reset(
Context.nCtx, NativeObject);
133 get {
return Native.Z3_goal_size(
Context.nCtx, NativeObject); }
143 Contract.Ensures(Contract.Result<
BoolExpr[]>() != null);
147 for (uint i = 0; i < n; i++)
158 get {
return Native.Z3_goal_num_exprs(
Context.nCtx, NativeObject); }
164 public bool IsDecidedSat
166 get {
return Native.Z3_goal_is_decided_sat(
Context.nCtx, NativeObject) != 0; }
172 public bool IsDecidedUnsat
174 get {
return Native.Z3_goal_is_decided_unsat(
Context.nCtx, NativeObject) != 0; }
182 Contract.Requires(ctx != null);
184 return new Goal(ctx, Native.Z3_goal_translate(
Context.nCtx, NativeObject, ctx.nCtx));
208 return Native.Z3_goal_to_string(
Context.nCtx, NativeObject);
227 internal Goal(
Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
229 internal Goal(
Context ctx,
bool models,
bool unsatCores,
bool proofs)
230 : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
232 Contract.Requires(ctx != null);
237 public DecRefQueue() : base() { }
238 public DecRefQueue(uint move_limit) : base(move_limit) { }
239 internal override void IncRef(
Context ctx, IntPtr obj)
241 Native.Z3_goal_inc_ref(ctx.nCtx, obj);
244 internal override void DecRef(
Context ctx, IntPtr obj)
246 Native.Z3_goal_dec_ref(ctx.nCtx, obj);
250 internal override void IncRef(IntPtr o)
256 internal override void DecRef(IntPtr o)
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
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.
Goal [] Subgoals
Retrieves the subgoals from the ApplyResult.
BoolExpr AsBoolExpr()
Goal to BoolExpr conversion.
IDecRefQueue Goal_DRQ
Goal DRQ
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
override string ToString()
Goal to string conversion.
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.
BoolExpr MkTrue()
The true Term.
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.
The main interaction with Z3 happens via the Context.
The exception base class for error reporting from Z3
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 ...
Goal Translate(Context ctx)
Translates (copies) the Goal to the target Context ctx .