35 public uint NumSubgoals
37 get {
return Native.Z3_apply_result_get_num_subgoals(
Context.nCtx, NativeObject); }
43 public Goal[] Subgoals
47 Contract.Ensures(Contract.Result<
Goal[]>() != null);
48 Contract.Ensures(Contract.Result<
Goal[]>().Length ==
this.NumSubgoals);
52 for (uint i = 0; i < n; i++)
53 res[i] =
new Goal(
Context, Native.Z3_apply_result_get_subgoal(
Context.nCtx, NativeObject, i));
65 Contract.Requires(m != null);
66 Contract.Ensures(Contract.Result<
Model>() != null);
68 return new Model(
Context, Native.Z3_apply_result_convert_model(
Context.nCtx, NativeObject, i, m.NativeObject));
76 return Native.Z3_apply_result_to_string(
Context.nCtx, NativeObject);
83 Contract.Requires(ctx != null);
88 public DecRefQueue() : base() { }
89 public DecRefQueue(uint move_limit) : base(move_limit) { }
90 internal override void IncRef(
Context ctx, IntPtr obj)
92 Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
95 internal override void DecRef(
Context ctx, IntPtr obj)
97 Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
101 internal override void IncRef(IntPtr o)
107 internal override void DecRef(IntPtr o)
override string ToString()
A string representation of the ApplyResult.
Model ConvertModel(uint i, Model m)
Convert a model for the subgoal i into a model for the original goal g, that the ApplyResult was obt...
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
A Model contains interpretations (assignments) of constants and functions.
The main interaction with Z3 happens via the Context.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...