diff options
author | Ken McMillan <unknown> | 2014-04-14 14:43:29 -0700 |
---|---|---|
committer | Ken McMillan <unknown> | 2014-04-14 14:43:29 -0700 |
commit | 37817c9f009f54b7203a0c0c132f9966b3b91bc8 (patch) | |
tree | e3ae5c471ec45f19c5c40ddcafef4994abfa816e /Source/Provers/SMTLib/TypeDeclCollector.cs | |
parent | 812961fd5f0cb1ca17737bebd9d09a318d38ccb6 (diff) |
Added /printFixedPoint option
Diffstat (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs')
-rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 18 |
1 files changed, 17 insertions, 1 deletions
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);
|