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 75a7f10f6c5ebea61944ddedcee957930ce2c586..9d0ae8e600d1f3d571e0034442e1fa6745680350 100644 (file)
--- 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 fa116bd96627b39b588604edee71f3a23e3ae9ae..fbc3bfa89d608a4ad63660e0d013563cc8203935 100644 (file)
--- 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 fa459311eb8ab0ddd02bfec9b31c48fc1629638d..bf346c67e63464e012a1f95f6bd0ccdc372c4817 100644 (file)
--- 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);
         }
       }
   }