diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-11-22 13:46:41 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-11-22 13:46:41 -0800 |
| commit | 4a45770d4a00399455b232c21c5cd10f3a2a93a6 (patch) | |
| tree | cfd726e7970a1481445a23c7e4cf5b6f4be33067 /Source/Core/ResolutionContext.cs | |
| parent | 1140d9e05274d8cc87f60602e317832cf05888fc (diff) | |
added support for handling duplicate axioms
Diffstat (limited to 'Source/Core/ResolutionContext.cs')
| -rw-r--r-- | Source/Core/ResolutionContext.cs | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 251ca1db..128df8c5 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -349,6 +349,26 @@ namespace Microsoft.Boogie { // not present in the relevant levels
return null;
}
+ Hashtable axioms = new Hashtable();
+
+ public void AddAxiom(Axiom axiom) {
+ string axiomName = QKeyValue.FindStringAttribute(axiom.Attributes, "name");
+ if (axiomName == null)
+ return;
+ var previous = (Axiom)axioms[axiomName];
+ if (previous == null) {
+ axioms.Add(axiomName, axiom);
+ }
+ else {
+ var r = (Axiom)SelectNonExtern(axiom, previous);
+ if (r == null) {
+ Error(axiom, "more than one declaration of axiom name: {0}", axiomName);
+ }
+ else {
+ axioms[axiomName] = r;
+ }
+ }
+ }
// ------------------------------ Functions/Procedures ------------------------------
|