added -fPIC flag for Java programs that want to use STP as a library

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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 1449e03c1101a2cbcab49dc3d9793416207f9dd5..396ffc042ab394cf85ce408dc69b608274eb8548 100644 (file)
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -10,23 +10,23 @@
 
 #OPTIMIZE     = -g -pg            # Debugging and gprof-style profiling
 OPTIMIZE      = -g                # Debugging
-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
 CFLAGS_BASE   = $(OPTIMIZE)
 
 # OPTION to compile CRYPTOMiniSAT
-# CRYPTOMINISAT  = true
-# CFLAGS_BASE    = $(OPTIMIZE) -DCRYPTOMINISAT
-# MTL            = ../sat/cryptominisat/mtl
-# SOLVER_INCLUDE = ../sat/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

diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp
index a7e29fdc0569ca0d6fceaea8c6f19bd459ef7b90..c183d21e7a4b460b2d11daf9c9e526f549ccb524 100644 (file)
--- a/src/to-sat/CallSAT.cpp
+++ b/src/to-sat/CallSAT.cpp
@@ -25,10 +25,10 @@ namespace BEEV
           {
             cl_size = CLAUSAL_BUCKET_LIMIT;
           }
-       else
-         {
-           cl_size = CLAUSAL_BUCKET_LIMIT-1;
-         }
+//     else
+//       {
+//         cl_size = CLAUSAL_BUCKET_LIMIT-1;
+//       }
 
         //If no clauses of size cl_size have been seen, then create a
         //bucket for that size

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index bea5b81c639c1e45ff4045d6a303d9a4015f6c91..f4877fd3b6535de63127c6e77f2753fffa113139 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -141,25 +141,25 @@ namespace BEEV
        newSolver.xorFinder = false;
 #endif
 
-       if(enable_clausal_abstraction && 
-          count++ >= input_clauselist_size*CLAUSAL_ABSTRACTION_CUTOFF)
-         {
-           //Arbitrary adding only x% of the clauses in the hopes of
-           //terminating early 
-           //      cout << "Percentage clauses added: " 
-           //           << percentage << endl;
-           bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
-           bm->GetRunTimes()->start(RunTimes::Solving);
-           newSolver.solve();
-           bm->GetRunTimes()->stop(RunTimes::Solving);
-           if(!newSolver.okay())
-             {
-               return false;         
-             }
-           count = 0;
-           flag  = 1;
-           bm->GetRunTimes()->start(RunTimes::SendingToSAT);
-         }
+//     if(enable_clausal_abstraction && 
+//        count++ >= input_clauselist_size*CLAUSAL_ABSTRACTION_CUTOFF)
+//       {
+//         //Arbitrary adding only x% of the clauses in the hopes of
+//         //terminating early 
+//         //      cout << "Percentage clauses added: " 
+//         //           << percentage << endl;
+//         bm->GetRunTimes()->stop(RunTimes::SendingToSAT);
+//         bm->GetRunTimes()->start(RunTimes::Solving);
+//         newSolver.solve();
+//         bm->GetRunTimes()->stop(RunTimes::Solving);
+//         if(!newSolver.okay())
+//           {
+//             return false;         
+//           }
+//         count = 0;
+//         flag  = 1;
+//         bm->GetRunTimes()->start(RunTimes::SendingToSAT);
+//       }
         if (newSolver.okay())
           {
             continue;