From f33e5329fc935e1d3ef3c1ef53bb4c09c96b1e23 Mon Sep 17 00:00:00 2001
From: Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com>
Date: Wed, 19 Oct 2011 23:40:36 +0530
Subject: Added a push+pop+unsat-core interface to SMTLib (for stratified
 inlining only)

---
 Source/Provers/SMTLib/TypeDeclCollector.cs | 79 +++++++++++++++++++++++++++---
 1 file changed, 73 insertions(+), 6 deletions(-)

(limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs')

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 23475242..0bc41c2a 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -36,6 +36,7 @@ void ObjectInvariant()
       Contract.Requires(namer != null);
       this.Namer = namer;
       this.Options = opts;
+      InitializeKnownDecls();
     }
 
     // not used
@@ -47,13 +48,79 @@ void ObjectInvariant()
     private readonly List<string/*!>!*/> AllDecls = new List<string/*!*/> ();
     private readonly List<string/*!>!*/> IncDecls = new List<string/*!*/> ();
 
-    private readonly HashSet<Function/*!*/>/*!*/ KnownFunctions = new HashSet<Function/*!*/>();
-    private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables = new HashSet<VCExprVar/*!*/>();
+    // In order to support push/pop interface of the theorem prover, the "known" declarations
+    // must be kept in a stack
 
-    private readonly HashSet<Type/*!*/>/*!*/ KnownTypes = new HashSet<Type>();
-    private readonly HashSet<string/*!*/>/*!*/ KnownStoreFunctions = new HashSet<string>();
-    private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions = new HashSet<string>();
-    private readonly HashSet<string> KnownLBL = new HashSet<string>();
+    private HashSet<Function/*!*/>/*!*/ KnownFunctions
+    {
+        get { return _KnownFunctions.Peek(); }
+    }
+
+    private HashSet<VCExprVar/*!*/>/*!*/ KnownVariables
+    {
+        get { return _KnownVariables.Peek(); }
+    }
+
+    private HashSet<Type/*!*/>/*!*/ KnownTypes
+    {
+        get { return _KnownTypes.Peek(); }
+    }
+
+    private HashSet<string/*!*/>/*!*/ KnownStoreFunctions
+    {
+        get { return _KnownStoreFunctions.Peek(); }
+    }
+
+    private HashSet<string/*!*/>/*!*/ KnownSelectFunctions
+    {
+        get { return _KnownSelectFunctions.Peek(); }
+    }
+
+    private HashSet<string> KnownLBL
+    {
+        get { return _KnownLBL.Peek(); }
+    }
+
+    // ------
+    private readonly Stack<HashSet<Function/*!*/>/*!*/> _KnownFunctions = new Stack<HashSet<Function/*!*/>>();
+    private readonly Stack<HashSet<VCExprVar/*!*/>/*!*/> _KnownVariables = new Stack<HashSet<VCExprVar/*!*/>>();
+
+    private readonly Stack<HashSet<Type/*!*/>/*!*/> _KnownTypes = new Stack<HashSet<Type>>();
+    private readonly Stack<HashSet<string/*!*/>/*!*/> _KnownStoreFunctions = new Stack<HashSet<string>>();
+    private readonly Stack<HashSet<string/*!*/>/*!*/> _KnownSelectFunctions = new Stack<HashSet<string>>();
+    private readonly Stack<HashSet<string>> _KnownLBL = new Stack<HashSet<string>>();
+
+    private void InitializeKnownDecls()
+    {
+        _KnownFunctions.Push(new HashSet<Function>());
+        _KnownVariables.Push(new HashSet<VCExprVar>());
+        _KnownTypes.Push(new HashSet<Type>());
+        _KnownStoreFunctions.Push(new HashSet<string>());
+        _KnownSelectFunctions.Push(new HashSet<string>());
+        _KnownLBL.Push(new HashSet<string>());
+    }
+
+    public void Push()
+    {
+        Contract.Assert(_KnownFunctions.Count > 0);
+        _KnownFunctions.Push(new HashSet<Function>(_KnownFunctions.Peek()));
+        _KnownVariables.Push(new HashSet<VCExprVar>(_KnownVariables.Peek()));
+        _KnownTypes.Push(new HashSet<Type>(_KnownTypes.Peek()));
+        _KnownStoreFunctions.Push(new HashSet<string>(_KnownStoreFunctions.Peek()));
+        _KnownSelectFunctions.Push(new HashSet<string>(_KnownSelectFunctions.Peek()));
+        _KnownLBL.Push(new HashSet<string>(_KnownLBL.Peek()));
+    }
+
+    public void Pop()
+    {
+        Contract.Assert(_KnownFunctions.Count > 1);
+        _KnownFunctions.Pop();
+        _KnownVariables.Pop();
+        _KnownTypes.Pop();
+        _KnownStoreFunctions.Pop();
+        _KnownSelectFunctions.Pop();
+        _KnownLBL.Pop();
+    }
 
     public List<string/*!>!*/> AllDeclarations { get {
       Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));
-- 
cgit v1.2.3