21using System.Diagnostics;
82 Debug.Assert(constraints !=
null);
83 Debug.Assert(constraints.All(c => c !=
null));
88 Debug.Assert(c !=
null);
89 Native.Z3_goal_assert(
Context.nCtx, NativeObject, c.NativeObject);
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); }
146 for (uint i = 0; i < n; i++)
157 get {
return Native.Z3_goal_num_exprs(
Context.nCtx, NativeObject); }
165 get {
return Native.Z3_goal_is_decided_sat(
Context.nCtx, NativeObject) != 0; }
173 get {
return Native.Z3_goal_is_decided_unsat(
Context.nCtx, NativeObject) != 0; }
184 return new Model(
Context, Native.Z3_goal_convert_model(
Context.nCtx, NativeObject, m.NativeObject));
186 return new Model(
Context, Native.Z3_goal_convert_model(
Context.nCtx, NativeObject, IntPtr.Zero));
195 Debug.
Assert(ctx !=
null);
197 return new Goal(ctx, Native.Z3_goal_translate(
Context.nCtx, NativeObject, ctx.nCtx));
221 return Native.Z3_goal_to_string(
Context.nCtx, NativeObject);
230 return Native.Z3_goal_to_dimacs_string(
Context.nCtx, NativeObject, (
byte)(include_names ? 1 : 0));
249 internal Goal(
Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx !=
null); }
251 internal Goal(Context ctx,
bool models,
bool unsatCores,
bool proofs)
252 : base(ctx, Native.
Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0)))
254 Debug.Assert(ctx !=
null);
257 internal class DecRefQueue : IDecRefQueue
259 public DecRefQueue() : base() { }
260 public DecRefQueue(uint move_limit) : base(move_limit) { }
261 internal override void IncRef(Context ctx, IntPtr obj)
263 Native.Z3_goal_inc_ref(ctx.nCtx, obj);
266 internal override void DecRef(Context ctx, IntPtr obj)
268 Native.Z3_goal_dec_ref(ctx.nCtx, obj);
272 internal override void IncRef(IntPtr o)
274 Context.
Goal_DRQ.IncAndClear(Context, o);
278 internal override void DecRef(IntPtr o)
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
uint NumSubgoals
The number of Subgoals.
Goal[] Subgoals
Retrieves the subgoals from the ApplyResult.
The main interaction with Z3 happens via the Context.
Tactic MkTactic(string name)
Creates a new Tactic.
BoolExpr MkTrue()
The true Term.
IDecRefQueue Goal_DRQ
Goal DRQ
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Model ConvertModel(Model m)
Convert a model for the goal into a model of the original goal from which this goal was derived.
Goal Simplify(Params p=null)
Simplifies the goal.
void Reset()
Erases all formulas from the given goal.
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
bool IsGarbage
Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
string ToDimacs(bool include_names=true)
Goal to DIMACS formatted string conversion.
uint Size
The number of formulas in the goal.
BoolExpr AsBoolExpr()
Goal to BoolExpr conversion.
uint NumExprs
The number of formulas, subformulas and terms in the goal.
override string ToString()
Goal to string conversion.
bool IsUnderApproximation
Indicates whether the goal is an under-approximation.
bool IsDecidedSat
Indicates whether the goal is empty, and it is precise or the product of an under approximation.
bool IsPrecise
Indicates whether the goal is precise.
Z3_goal_prec Precision
The precision of the goal.
bool IsOverApproximation
Indicates whether the goal is an over-approximation.
Goal Translate(Context ctx)
Translates (copies) the Goal to the target Context ctx .
BoolExpr[] Formulas
The formulas in the goal.
void Add(params BoolExpr[] constraints)
Alias for Assert.
bool Inconsistent
Indicates whether the goal contains ‘false’.
bool IsDecidedUnsat
Indicates whether the goal contains ‘false’, and it is precise or the product of an over approximatio...
uint Depth
The depth of the goal.
A Model contains interpretations (assignments) of constants and functions.
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....
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
The exception base class for error reporting from Z3
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...