From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 29 Apr 2012 10:49:41 +0000 (+0000)
Subject: Potentiall rewriting improvement. Not sure yet.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1d1eed71df76a50ce90d8b35f341dcd320767ff2;p=francis%2Fstp.git

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 e6bd137..cb6fbab 100644
--- 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);