From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 20 Mar 2011 02:36:09 +0000 (+0000)
Subject: Improvement. More cases for the simplifying node factory.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=0001fe91f1d099880cd2cbaa7ead3e8f331d759c;p=francis%2Fstp.git

Improvement. More cases for the simplifying node factory.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 47f2e16..37ac0a8 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -544,6 +544,43 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 		break;
 	}
 
+	case BEEV::BVAND:
+	  {
+
+	    bool oneFound=false;
+	    bool zeroFound=false;
+
+	    for (int i = 0; i < children.size(); i++)
+            {
+              if (children[i].GetKind() == BEEV::BVCONST)
+                {
+                if (CONSTANTBV::BitVector_is_full(children[i].GetBVConst()))
+                  oneFound = true;
+                else if (CONSTANTBV::BitVector_is_empty(children[i].GetBVConst()))
+                  zeroFound = true;
+                }
+            }
+
+	    if (zeroFound)
+	      return bm.CreateZeroConst(width);
+
+	    if (oneFound)
+	      {
+	        ASTVec new_children;
+                for (int i = 0; i < children.size(); i++)
+                {
+                  if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst()))
+                    new_children.push_back(children[i]);
+                }
+
+                assert(new_children.size() != 0); // constant. Should have been handled earlier.
+                if (new_children.size() == 1)
+                  return new_children[0];
+                else
+                  result = hashing.CreateTerm(kind, width, new_children);
+	      }
+	  }
+	  break;
 
 	case BEEV::BVSX:
 	{
@@ -552,30 +589,24 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 		break;
 	}
 
-
 	case BEEV::BVNEG:
-	{
-		switch (children[0].GetKind())
-		{
-
-		case BEEV::BVNEG:
-			result = children[0][0];
-			break;
-		default: // quieten compiler.
-			break;
-		}
-	}
+	  if (children[0].GetKind() == BEEV::BVNEG)
+	    return children[0][0];
 	break;
 
+        case BEEV::BVUMINUS:
+          if (children[0].GetKind() == BEEV::BVUMINUS)
+            return children[0][0];
+        break;
 
 	case BEEV::BVMOD:
-		if (children[1].isConstant())
-		{
-			ASTNode one = bm.CreateOneConst(width);
-			if (children[1] == one)
-				result = bm.CreateZeroConst(width);
-		}
-		break;
+        if (children[1].isConstant())
+        {
+                ASTNode one = bm.CreateOneConst(width);
+                if (children[1] == one)
+                        result = bm.CreateZeroConst(width);
+        }
+        break;
 
 
 	case BEEV::READ:
@@ -589,6 +620,7 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 		break;
 	}
 
+
 	if (result.IsNull())
 		result = hashing.CreateTerm(kind, width, children);