21 using System.Diagnostics.Contracts;
29 [ContractVerification(
true)]
35 public uint NumSubgoals
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++)
65 Contract.Requires(m != null);
66 Contract.Ensures(Contract.Result<
Model>() != null);
83 Contract.Requires(ctx != null);
88 public override void IncRef(Context ctx, IntPtr obj)
90 Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
93 public override void DecRef(Context ctx, IntPtr obj)
95 Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
99 internal override void IncRef(IntPtr o)
101 Context.ApplyResult_DRQ.IncAndClear(Context, o);
105 internal override void DecRef(IntPtr o)
107 Context.ApplyResult_DRQ.Add(o);
override string ToString()
A string representation of the ApplyResult.
static Z3_model Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, uint a2, Z3_model a3)
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...
static uint Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1)
static string Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1)
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.
static Z3_goal Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, uint a2)
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 ...