From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 28 Feb 2011 13:31:43 +0000 (+0000)
Subject: Improvement. Enable ITE context simplifications again.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=b5e85a4802cfe40be34657619d86acdda78075fe;p=francis%2Fstp.git

Improvement. Enable ITE context simplifications again.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1179 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/simplifier/UseITEContext.h b/src/simplifier/UseITEContext.h
index 5c16e25..47d3836 100644
--- a/src/simplifier/UseITEContext.h
+++ b/src/simplifier/UseITEContext.h
@@ -37,26 +37,23 @@ namespace BEEV
         }
       else
         context.insert(n);
-
-        //ASTNodeSet::iterator it = context.begin();
-        //cout << "NEW CONTEXT";
-        //while(it!=context.end())
-        //  {
-         //   cout << *it;
-         //   it++;
-         // }
     }
 
+    // Unfortunately there can be a lot of paths through a small formula.
+    // So we limit how often each node is visited.
+
     ASTNode
-    visit(const ASTNode &n, ASTNodeSet& visited, ASTNodeSet& context)
+    visit(const ASTNode &n, map<ASTNode,int>& visited, ASTNodeSet& visited_empty, ASTNodeSet& context)
     {
       if (n.isConstant())
         return n;
 
-      ASTNodeSet::iterator it;
-      if (context.size() == 0 && ((it = visited.find(n)) != visited.end()))
+      if (context.size() == 0 && visited_empty.find(n) != visited_empty.end())
         return n;
 
+      if (context.size() == 0)
+        visited_empty.insert(n);
+
       if (context.find(n) != context.end())
         return ASTTrue;
 
@@ -66,21 +63,26 @@ namespace BEEV
       if (n.isAtom())
         return n;
 
+      {
+          if (visited[n]++ > 10)
+            return n;
+      }
+
       ASTVec new_children;
 
       if (n.GetKind() == ITE)
         {
-            ASTNodeSet lhsContext(context), rhsContext(context);
+          ASTNodeSet lhsContext(context), rhsContext(context);
             addToContext(n[0],lhsContext);
             addToContext(nf->CreateNode(NOT,n[0]),rhsContext);
-            new_children.push_back(visit(n[0], visited,context));
-            new_children.push_back(visit(n[1], visited,lhsContext));
-            new_children.push_back(visit(n[2], visited,rhsContext));
+            new_children.push_back(visit(n[0], visited,visited_empty, context));
+            new_children.push_back(visit(n[1], visited,visited_empty, lhsContext));
+            new_children.push_back(visit(n[2], visited,visited_empty, rhsContext));
         }
       else
         {
           for (int i = 0; i < n.GetChildren().size(); i++)
-            new_children.push_back(visit(n[i], visited, context));
+            new_children.push_back(visit(n[i], visited, visited_empty, context));
         }
 
       ASTNode result;
@@ -92,9 +94,7 @@ namespace BEEV
       else
         result = n;
 
-      visited.insert(n);
       return result;
-
     }
 
   public:
@@ -103,9 +103,10 @@ namespace BEEV
     topLevel(const ASTNode& n)
     {
       runtimes->start(RunTimes::UseITEContext);
-      ASTNodeSet visited;
+      map<ASTNode,int> visited;
       ASTNodeSet context;
-      ASTNode result= visit(n,visited,context);
+      ASTNodeSet empty;
+      ASTNode result= visit(n,visited,empty,context);
       runtimes->stop(RunTimes::UseITEContext);
       return result;
     }