From 239f0413308b0098307df9113106bc07b3916232 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 10 Jan 2010 21:07:20 +0000
Subject: [PATCH] BitBlast.cpp: Was generating XOR-clauses by default since
 this is very good for CryptoMiniSAT2. However, forgot put it under flag. Now
 corrected.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@551 e59a4935-1847-0410-ae03-e826735625c1
---
 scripts/Makefile.common | 16 ++++------------
 src/to-sat/BitBlast.cpp | 37 ++++++++++++++++++-------------------
 2 files changed, 22 insertions(+), 31 deletions(-)

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index ac03650..770273c 100644
--- 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 fbc3bfa..3901298 100644
--- 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;
   }
 
-- 
2.47.3