Improvement. Nicer handling of bit-vector not in bvxors.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 647e64c16b78b12ed4fc8b2145a6126e475b8a7b..f6882098a39c035544171f981c5cdadf0ebcbd57 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -1089,13 +1089,14 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &
         if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst()))
           result = NodeFactory::CreateTerm(BVNEG, width, children[1]);
 
-        if (children[1].GetKind() == BVNEG && children[1][0] == children[0])
-          result = bm.CreateMaxConst(width);
-
-        if (children[0].GetKind() == BVNEG && children[0][0] == children[1])
-          result = bm.CreateMaxConst(width);
-        if ( width >= 3 &&  children.size() ==2 && children[0].GetKind() == BVNEG && children[1].GetKind() == BVNEG )
-          result =  NodeFactory::CreateTerm(BVXOR,width,children[1][0],children[0][0]);//133 -> 133
+        if (children[1].GetKind() == BVNEG)
+          {
+            result = NodeFactory::CreateTerm(BVNEG, width, NodeFactory::CreateTerm(BVXOR, width, children[0], children[1][0]));
+      }
+        else if (children[0].GetKind() == BVNEG)
+          {
+            result = NodeFactory::CreateTerm(BVNEG, width, NodeFactory::CreateTerm(BVXOR, width, children[1], children[0][0]));
+          }
       }
     break;