Bugfix. I didn't realise that the Flatten function didn't flatten BVOR/BVANDs. When...

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

diff --git a/src/simplifier/consteval.cpp b/src/simplifier/consteval.cpp
index a5d8b6692051eaff639d1d223a98359363b323e6..a84b029de731d65267e957c8620ab710cb034066 100644 (file)
--- 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 64e829f75b56d53e61ea3e34473fadab5c2699b8..27fc2f4a35c593e7691e42835139ca3a03d58b17 100644 (file)
--- 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;
             }