From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 9 Dec 2009 18:02:28 +0000 (+0000)
Subject: added -fPIC flag for Java programs that want to use STP as a library
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=f604d3d3136f991106d923cfc56977983852fbb9;p=francis%2Fstp.git

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 1449e03..396ffc0 100644
--- 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 a7e29fd..c183d21 100644
--- 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 bea5b81..f4877fd 100644
--- 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;