BitBlast.cpp: Was generating XOR-clauses by default since this is very good for Crypt...

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index ac03650616f4c3a421eb41f3fac4cba6f8639461..770273c5ad59a1b674e8cb3248b3282d2138e91f 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -17,17 +17,11 @@ OPTIMIZE      = -O3               # Maximum optimization
 #CFLAGS_M32   = -m32
 CFLAGS_BASE   = $(OPTIMIZE)
 
-# OPTION to compile CRYPTOMiniSAT
-# CRYPTOMINISAT  = true
-# CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT
-# MTL            = ../sat/cryptominisat/mtl
-# SOLVER_INCLUDE = ../sat/cryptominisat
-
 # OPTION to compile CRYPTOMiniSAT version 2.x
-#CRYPTOMINISAT2 = true
-#CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
-#MTL            = ../sat/cryptominisat2/mtl
-#SOLVER_INCLUDE = ../sat/cryptominisat2
+# CRYPTOMINISAT2 = true
+# CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT2
+# MTL            = ../sat/cryptominisat2/mtl
+# SOLVER_INCLUDE = ../sat/cryptominisat2
 
 # OPTION to compile MiniSAT
 CORE          = true
@@ -35,14 +29,12 @@ CFLAGS_BASE   = $(OPTIMIZE) -DCORE
 MTL            = ../sat/mtl
 SOLVER_INCLUDE = ../sat/core
 
-
 # OPTION to compile UNSOUND MiniSAT
 #UNSOUND       = true
 #CFLAGS_BASE   = $(OPTIMIZE) -DUNSOUND
 #MTL            = ../sat/mtl
 #SOLVER_INCLUDE = ../sat/unsound
 
-
 # OPTION to compile Simplifying MiniSAT
 # SIMP          = true
 # CFLAGS_BASE   = $(OPTIMIZE) -DSIMP

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index fbc3bfa89d608a4ad63660e0d013563cc8203935..39012989e08402c3008eca24de9cf60724ed9025 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -729,19 +729,10 @@ namespace BEEV
     // worth doing explicitly (e.g., a = b, a = ~b, etc.)
     else
       {
-//     return _bm->CreateSimpForm(OR, 
-//                                _bm->CreateSimpForm(AND, a, b), 
-//                                _bm->CreateSimpForm(AND, b, c), 
-//                                _bm->CreateSimpForm(AND, a, c));
-        return 
-         _bm->CreateSimpForm(AND, 
-                             _bm->CreateSimpForm(OR, a, b),
-                             //_bm->CreateSimpForm(XOR,a,b)),
-                             _bm->CreateSimpForm(OR, b, c),
-                             //_bm->CreateSimpForm(XOR,b,c)),
-                             _bm->CreateSimpForm(OR, a, c)
-                             //_bm->CreateSimpForm(XOR,a,c)
-                             );      
+       return _bm->CreateSimpForm(OR, 
+                                  _bm->CreateSimpForm(AND, a, b), 
+                                  _bm->CreateSimpForm(AND, b, c), 
+                                  _bm->CreateSimpForm(AND, a, c));
       }
   }
 
@@ -749,11 +740,16 @@ namespace BEEV
                           const ASTNode& yi,
                           const ASTNode& cin)
   {
-    ASTNode S0 = _bm->CreateSimpForm(XOR,
-                                     //_bm->CreateSimpForm(XOR, xi, yi),
-                                    xi,
-                                    yi,
-                                     cin);
+    ASTNode S0;
+    
+#ifdef CRYPTOMINISAT2
+    S0 = _bm->CreateSimpForm(XOR, xi, yi, cin);
+#else
+    S0 = _bm->CreateSimpForm(XOR,
+                            _bm->CreateSimpForm(XOR, xi, yi),
+                            cin);
+#endif
+
     return S0;
   }
 
@@ -955,8 +951,11 @@ namespace BEEV
         bit_comparisons.push_back(prev_eq_bit);
       }
     ASTNode output =
+#ifdef CRYPTOMINISAT2
       _bm->CreateSimpForm(XOR, bit_comparisons);
-
+#else
+      _bm->CreateSimpForm(OR, bit_comparisons);
+#endif
     return output;
   }