From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 11 Dec 2009 00:27:54 +0000 (+0000)
Subject: converting NOT(a) into XOR(a, true). Helps with bio. Breaks test000013.cvc
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=249891e27248ebbdc0eeed12d4a27a266cd0e7f6;p=francis%2Fstp.git

converting NOT(a) into XOR(a, true). Helps with bio. Breaks test000013.cvc

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 75a7f10..9d0ae8e 100644
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -11,7 +11,7 @@
 #OPTIMIZE     = -g -pg            # Debugging and gprof-style profiling
 OPTIMIZE      = -g                # Debugging
 #OPTIMIZE      = -O3 -fPIC         # Maximum optimization
-#OPTIMIZE      = -O3 -march=native # Maximum optimization
+#OPTIMIZE      = -O3 -march=native -fomit-frame-pointer # Maximum optimization
 #OPTIMIZE      = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
 OPTIMIZE      = -O3               # Maximum optimization
 #CFLAGS_M32   = -m32
diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index fa116bd..fbc3bfa 100644
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -925,6 +925,7 @@ namespace BEEV
     ASTVec bit_comparisons;
     bit_comparisons.push_back(this_compare_bit);
     
+    //(lit IFF rit) is the same as (NOT(lit) XOR rit)
     ASTNode prev_eq_bit = 
       _bm->CreateSimpForm(XOR, 
 			  _bm->CreateSimpForm(NOT,*lit), 
@@ -932,13 +933,14 @@ namespace BEEV
     for(lit++, rit++; lit < litend; lit++, rit++)
       {
         this_compare_bit = 
-          _bm->CreateSimpForm(AND, _bm->CreateSimpNot(*lit), *rit);
+          _bm->CreateSimpForm(AND, 
+			      _bm->CreateSimpNot(*lit), 
+			      *rit);
 
         ASTNode thisbit_output = 
           _bm->CreateSimpForm(AND, this_compare_bit, prev_eq_bit);
         bit_comparisons.push_back(thisbit_output);
-
-        // (neg(lit) OR rit)(lit OR neg(rit))
+  
         ASTNode this_eq_bit = 
           _bm->CreateSimpForm(AND,
                               _bm->CreateSimpForm(XOR,
@@ -1105,7 +1107,9 @@ namespace BEEV
         return n;
       }
     else
-      return _bm->CreateSimpForm(XOR, 
-				 _bm->CreateSimpForm(NOT,*lit), *rit);
+      {
+	return _bm->CreateSimpForm(XOR, 
+				   _bm->CreateSimpForm(NOT,*lit), *rit);
+      }
   }
 } // BEEV namespace
diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index fa45931..bf346c6 100644
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -139,7 +139,8 @@ namespace BEEV
         }
       default:
         {
-          return CreateNode(NOT, form);
+	  //return CreateNode(NOT, form);
+          return CreateNode(XOR, ASTTrue, form);
         }
       }
   }