From 37817c9f009f54b7203a0c0c132f9966b3b91bc8 Mon Sep 17 00:00:00 2001
From: Ken McMillan <unknown>
Date: Mon, 14 Apr 2014 14:43:29 -0700
Subject: Added /printFixedPoint option

---
 Source/Provers/SMTLib/TypeDeclCollector.cs | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

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

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 2bf8fa22..30363102 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -90,7 +90,19 @@ void ObjectInvariant()
     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>>();
-
+		
+	// lets RPFP checker capture decls	
+	public abstract class DeclHandler {
+		public abstract void VarDecl(VCExprVar v);
+		public abstract void FuncDecl(Function f);
+	}
+		
+	private DeclHandler declHandler = null;
+
+	public void SetDeclHandler(DeclHandler _d){
+		declHandler = _d;
+	}
+		
     private void InitializeKnownDecls()
     {
         _KnownFunctions.Push(new HashSet<Function>());
@@ -182,6 +194,8 @@ void ObjectInvariant()
       if (KnownFunctions.Contains(func))
         return;
       KnownFunctions.Add(func);
+	  if(declHandler != null)
+		declHandler.FuncDecl(func);
     }
 
     public void RegisterRelation(Function func)
@@ -242,6 +256,8 @@ void ObjectInvariant()
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
         AddDeclaration(decl);
         KnownVariables.Add(node);
+		if(declHandler != null)
+			declHandler.VarDecl(node);
       }
 
       return base.Visit(node, arg);
-- 
cgit v1.2.3