diff options
| author |  Ken McMillan <unknown> | 2014-05-26 14:33:08 -0700 |
|---|---|---|
| committer | Ken McMillan <unknown> | 2014-05-26 14:33:08 -0700 |
| commit | 7d9165d6b61e7475b973d3bf86d063dcc4a454d1 (patch) | |
| tree | 0aa2ad477785c280b3ee165bff71c8abc479b126 /Source/VCGeneration/RPFP.cs | |
| parent | 14e663bd2f9bccd191cfb6f9c72c7efa4e6b4e33 (diff) | |
Conjecture printing for duality and child user time tracking.
Diffstat (limited to 'Source/VCGeneration/RPFP.cs')
| -rw-r--r-- | Source/VCGeneration/RPFP.cs | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs index e7df7be6..ed3842d5 100644 --- a/Source/VCGeneration/RPFP.cs +++ b/Source/VCGeneration/RPFP.cs @@ -325,6 +325,17 @@ namespace Microsoft.Boogie return res;
}
+ /** This represents a conjecture that a given node is upper-boudned
+ by bound. */
+ public class Conjecture
+ {
+ public Node node;
+ public Transformer bound;
+ }
+
+ /** This is a list of conjectures generated during solving. */
+
+ public List<Conjecture> conjectures = new List<Conjecture>();
/** Construct an RPFP graph with a given interpolating prover context. It is allowed to
have multiple RPFP's use the same context, but you should never have teo RPFP's
|