From 6b8b0680846d02bc27d9529b382bd1b483ebc8d8 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 2 Jan 2011 02:29:15 +0000
Subject: [PATCH] Bugfix. I didn't realise that the Flatten function didn't
 flatten BVOR/BVANDs. When I replaced the function, it did. Flattening these
 took a long time. This patch: (1) performs the flatten upfront, (2) allows
 BVOR/BVAND >2 arity.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1046 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/consteval.cpp  | 35 ++++++++++++++++++++++---------
 src/simplifier/simplifier.cpp | 39 +++++++++++++++++++++++------------
 2 files changed, 51 insertions(+), 23 deletions(-)

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index a5d8b66..a84b029 100644
--- a/src/simplifier/consteval.cpp
+++ b/src/simplifier/consteval.cpp
@@ -167,19 +167,34 @@ namespace BEEV
 
       case BVAND:
         {
-          assert(2==t.Degree());
-          output = CONSTANTBV::BitVector_Create(inputwidth, true);
-          CONSTANTBV::Set_Intersection(output, tmp0, tmp1);
-          OutputNode = _bm->CreateBVConst(output, outputwidth);
-          break;
+        	assert(1 <= t.Degree());
+
+        	output = CONSTANTBV::BitVector_Create(inputwidth, true);
+        	CONSTANTBV::BitVector_Fill(output);
+
+            for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++)
+              {
+                CBV kk = (*it).GetBVConst();
+                CONSTANTBV::Set_Intersection(output, output, kk);
+              }
+
+            OutputNode = _bm->CreateBVConst(output, outputwidth);
+            break;
         }
       case BVOR:
         {
-          assert(2==t.Degree());
-          output = CONSTANTBV::BitVector_Create(inputwidth, true);
-          CONSTANTBV::Set_Union(output, tmp0, tmp1);
-          OutputNode = _bm->CreateBVConst(output, outputwidth);
-          break;
+        	assert(1 <= t.Degree());
+
+        	output = CONSTANTBV::BitVector_Create(inputwidth, true);
+
+            for (ASTVec::iterator it = children.begin(), itend = children.end(); it != itend; it++)
+              {
+                CBV kk = (*it).GetBVConst();
+                CONSTANTBV::Set_Union(output, output, kk);
+              }
+
+            OutputNode = _bm->CreateBVConst(output, outputwidth);
+            break;
         }
       case BVXOR:
         {
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 64e829f..27fc2f4 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1655,14 +1655,22 @@ namespace BEEV
 		if (k != SYMBOL) // const and symbols need to be created specially.
 		{
 			ASTVec v;
-			v.reserve(actualInputterm.Degree());
-			for (unsigned i = 0; i < actualInputterm.Degree(); i++)
-				if (inputterm[i].GetType() == BITVECTOR_TYPE)
-					v.push_back(SimplifyTerm(inputterm[i], VarConstMap));
-				else if (inputterm[i].GetType() == BOOLEAN_TYPE)
-					v.push_back(SimplifyFormula(inputterm[i], VarConstMap));
+			ASTVec toProcess = actualInputterm.GetChildren();
+			if (actualInputterm.GetKind() == BVAND || actualInputterm.GetKind() == BVOR)
+			{
+				// If we didn't flatten these, then we'd start flattening each of these
+				// from the bottom up. Potentially creating tons of the nodes along the way.
+				toProcess = FlattenKind(actualInputterm.GetKind(), toProcess);
+			}
+
+			v.reserve(toProcess.size());
+			for (unsigned i = 0; i < toProcess.size(); i++)
+				if (toProcess[i].GetType() == BITVECTOR_TYPE)
+					v.push_back(SimplifyTerm(toProcess[i], VarConstMap));
+				else if (toProcess[i].GetType() == BOOLEAN_TYPE)
+					v.push_back(SimplifyFormula(toProcess[i], VarConstMap));
 				else
-					v.push_back(inputterm[i]);
+					v.push_back(toProcess[i]);
 
 			assert(v.size() > 0);
 			if (v != actualInputterm.GetChildren()) // short-cut.
@@ -2317,11 +2325,16 @@ namespace BEEV
               break;
             case BVAND:
             case BVOR:
-              assert(a0.Degree() == 2);
-              output = 
-                nf->CreateTerm(a0.GetKind(), len,
-                                nf->CreateTerm(BVSX, len, a0[0], a1),
-                                nf->CreateTerm(BVSX, len, a0[1], a1));
+            {
+              ASTVec c = a0.GetChildren();
+              ASTVec newChildren;
+              for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
+			  {
+				  newChildren.push_back(nf->CreateTerm(BVSX, len, *it, a1));
+			  }
+
+              output =  nf->CreateTerm(a0.GetKind(), len, newChildren );
+            }
               break;
             case BVPLUS:
               {
@@ -2476,7 +2489,7 @@ namespace BEEV
               break;
             default:
               SortByArith(o);
-              output = makeTower(inputterm.GetKind(),o );
+              output = nf->CreateTerm(inputterm.GetKind(),inputterm.GetValueWidth(), o );
               break;
             }
 
-- 
2.47.3