made -fPIC and -march=native optional

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 70d7bc51c28fed1a805a34626b247e3e9a262dc8..4f8674a48d7571af69cb6ed92bfc6aa2087fb89c 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -10,7 +10,8 @@
 
 #OPTIMIZE     = -g -pg            # Debugging and gprof-style profiling
 OPTIMIZE      = -g                # Debugging
-OPTIMIZE      = -O3 -fPIC         # Maximum optimization
+OPTIMIZE      = -O3               # Maximum optimization
+#OPTIMIZE      = -O3 -fPIC         # Maximum optimization
 #OPTIMIZE      = -O3 -march=native # Maximum optimization
 #OPTIMIZE     = -O3 -march=native -DNDEBUG -DLESSBYTES_PERNODE
 #CFLAGS_M32   = -m32

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index 8eac6312d5d349b37dbc6144ae7e41c5cf337178..fa116bd96627b39b588604edee71f3a23e3ae9ae 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -1034,7 +1034,8 @@ namespace BEEV
         }
       case BVGT:
         {
-          return _bm->CreateSimpNot(BBBVLE(left, right, false));
+          //return _bm->CreateSimpNot(BBBVLE(left, right, false));
+          return BBBVLE(right, left, false, true);
           break;
         }
       case BVLT:

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/SimpBool.cpp
index 273b46a000d92246e32eea98ff3f61806e56161a..fa459311eb8ab0ddd02bfec9b31c48fc1629638d 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/SimpBool.cpp
@@ -481,17 +481,6 @@ namespace BEEV
       {
         retval = CreateSimpAndOr(1, child0, child1);
       }
-//     //ITE (x, !y, y) == x XOR y
-//     else if (NOT == child1.GetKind() && (child1[0] == child2))
-//       {
-//     retval = CreateSimpXor(child0, child2);
-//       }
-//     // ITE (x, y, !y) == x IFF y.  I think other cases are covered
-//     // by XOR/IFF optimizations
-//     else if (NOT == child2.GetKind() && (child2[0] == child1)) 
-//       {
-//     retval = CreateSimpXor(CreateSimpNot(child0), child2);
-//       }
     else
       {
        ASTNode left  = CreateNode(AND, child0, child1);

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 3a257cb748d5ce094f1118cd09539ddf0360fd89..d2ac1e980eb6a96f2a871ac88382cfab97b8d981 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -137,7 +137,7 @@ namespace BEEV
 
 #if defined CRYPTOMINISAT2
        newSolver.set_gaussian_decision_until(100);
-       newSolver.performReplace = false;
+       newSolver.performReplace = true;
        newSolver.xorFinder = false;
 #endif