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);
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)
244 internal override void DecRef(
Context ctx, IntPtr 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 ....
static void Z3_goal_dec_ref(Z3_context a0, Z3_goal a1)
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.
BoolExpr AsBoolExpr()
Goal to BoolExpr conversion.
IDecRefQueue Goal_DRQ
Goal DRQ
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)
BoolExpr MkTrue()
The true Term.
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 Params objects 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 void Z3_goal_inc_ref(Z3_context a0, Z3_goal a1)
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.
static Z3_goal Z3_mk_goal(Z3_context a0, int a1, int a2, int a3)
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 .