diff options
| author |  wuestholz <unknown> | 2014-04-21 13:21:52 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-04-21 13:21:52 +0200 |
| commit | b17515ca23fc7f5ae1fb8e6642366f761d0eeacf (patch) | |
| tree | 1f1b42a681dab35e9d6aa02bc1a79d01c113c82f /Source/Core/ResolutionContext.cs | |
| parent | c29f461136e76fd406677e1e12245ee69368190f (diff) | |
Add support for assumption variables.
Diffstat (limited to 'Source/Core/ResolutionContext.cs')
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 403803a3..eb27c82a 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -265,6 +265,48 @@ namespace Microsoft.Boogie { public readonly Hashtable /*string->Variable*//*!*/ VarSymbols = new Hashtable /*string->Variable*/();
public /*maybe null*/ VarContextNode ParentContext;
public readonly bool Opaque;
+ readonly ISet<string> assignedAssumptionVariables = new HashSet<string>();
+
+ public bool HasVariableBeenAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ if (assignedAssumptionVariables.Contains(name))
+ {
+ return true;
+ }
+ else if (ParentContext != null)
+ {
+ return ParentContext.HasVariableBeenAssigned(name);
+ }
+ else
+ {
+ return false;
+ }
+ }
+
+ public bool MarkVariableAsAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ if (VarSymbols.Contains(name))
+ {
+ if (assignedAssumptionVariables.Contains(name))
+ {
+ return false;
+ }
+ assignedAssumptionVariables.Add(name);
+ return true;
+ }
+ else if (ParentContext != null)
+ {
+ return ParentContext.MarkVariableAsAssigned(name);
+ }
+ else
+ {
+ return false;
+ }
+ }
public VarContextNode(/*maybe null*/ VarContextNode parentContext, bool opaque) {
ParentContext = parentContext;
@@ -349,6 +391,22 @@ namespace Microsoft.Boogie { // not present in the relevant levels
return null;
}
+
+ public bool HasVariableBeenAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ return varContext.HasVariableBeenAssigned(name);
+ }
+
+ public void MarkVariableAsAssigned(string name)
+ {
+ Contract.Requires(name != null);
+
+ var success = varContext.MarkVariableAsAssigned(name);
+ Contract.Assume(success);
+ }
+
Hashtable axioms = new Hashtable();
public void AddAxiom(Axiom axiom) {
|