Potentiall rewriting improvement. Not sure yet.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index e6bd13762c4b6b0522690d807d89bcdb70a02788..cb6fbabb0a58ec81e952b4d0f2a409797201f3c9 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1032,6 +1032,17 @@ namespace BEEV
               }
           }
       }
+    if (k2 == ITE && (in2[1] == in1) && in1.GetType()== BITVECTOR_TYPE)
+      {
+        ASTNode eq = nf->CreateNode(EQ, in1,in2[2]);
+        return  nf->CreateNode(OR,in2[0],eq );
+      }
+
+    if (k2 == ITE && (in2[2] == in1) && in1.GetType()== BITVECTOR_TYPE)
+      {
+        ASTNode eq = nf->CreateNode(EQ, in1,in2[1]);
+        return  nf->CreateNode(OR,nf->CreateNode(NOT,in2[0]),eq );
+      }
 
     //last resort is to CreateNode
     return nf->CreateNode(EQ, in1, in2);