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 DecRefQueue() : base() { }
89 public DecRefQueue(uint move_limit) : base(move_limit) { }
90 internal override void IncRef(
Context ctx, IntPtr obj)
95 internal override void DecRef(
Context ctx, IntPtr obj)
101 internal override void IncRef(IntPtr o)
107 internal override void DecRef(IntPtr 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)
static void Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1)
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)
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
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...
static void Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1)
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 ...