From: trevor_hansen Date: Tue, 13 Apr 2010 15:23:19 +0000 (+0000) Subject: If STP is compiled with minisat-core, add a command line option to enable simplifying... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ac47bff2f3cf578c3cd1bfad40581e326ad0ab6d;p=francis%2Fstp.git If STP is compiled with minisat-core, add a command line option to enable simplifying minisat. This removes the need to separately compile a "simplifying minisat" version. We now have two versions of STP: one for cryptominisat1/2 another for minisat/simplifying minisat. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@670 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index fe16bb2..05a2c4e 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -35,14 +35,6 @@ ifeq ($(SAT),minisat) SOLVER_INCLUDE = $(TOP)/src/sat/core endif -# OPTION to compile Simplifying MiniSAT -ifeq ($(SAT),simp) - SIMP = true - CFLAGS_BASE = $(OPTIMIZE) -DSIMP - MTL = $(TOP)/src/sat/mtl - SOLVER_INCLUDE = $(TOP)/src/sat/simp -endif - SHELL=/bin/bash # You can compile using make STATIC=true to compile a statically diff --git a/scripts/configure b/scripts/configure index d3773a3..039f084 100755 --- a/scripts/configure +++ b/scripts/configure @@ -21,16 +21,13 @@ while [ $# -gt 0 ]; do echo "Using g++ instead of gcc";; --with-minisat-core) SAT=minisat;; - --with-minisat-simp) - SAT=simp;; --with-cryptominisat2) SAT=cryptominisat2;; *) echo "Usage: $0 [options]" echo " --with-prefix=/prefix/path Install STP at the specified path" echo " --with-g++=/path/to/g++ Use g++ at the specified path" - echo " --with-minisat-core Use core MiniSAT solver (default)" - echo " --with-minisat-simp Use simplifying MiniSAT solver" + echo " --with-minisat-core Use core MiniSAT solver (default), runtime option to use simplifying" echo " --with-cryptominisat2 Use CRYPTOMiniSAT 2.x solver" echo "$0 failed" exit 1;; diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 84aafb2..d81daee 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -21,7 +21,7 @@ namespace BEEV { bm->CreateNode(NOT, query)); //solver instantiated here -#if defined CORE || defined CRYPTOMINISAT || defined CRYPTOMINISAT2 +#if defined CRYPTOMINISAT || defined CRYPTOMINISAT2 MINISAT::Solver NewSolver; #endif @@ -32,8 +32,16 @@ namespace BEEV { } #endif -#ifdef SIMP - MINISAT::SimpSolver NewSolver; +#if defined CORE + MINISAT::Solver *newS; + if (bm->UserFlags.solver_to_use == UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER) + newS = new MINISAT::SimpSolver(); + else if (bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_SOLVER) + newS = new MINISAT::Solver(); + else + FatalError("unknown option"); + + MINISAT::Solver& NewSolver = *newS; #endif if(bm->UserFlags.stats_flag) @@ -41,16 +49,24 @@ namespace BEEV { NewSolver.verbosity = 1; } + SOLVER_RETURN_TYPE result; if(bm->UserFlags.num_absrefine_flag) { - return UserGuided_AbsRefine(NewSolver, + result = UserGuided_AbsRefine(NewSolver, original_input); } else { - return TopLevelSTPAux(NewSolver, + result = TopLevelSTPAux(NewSolver, original_input, original_input); } + +#if defined CORE + delete newS; +#endif + + return result; + } //End of TopLevelSTP() //Acceps a query, calls the SAT solver and generates Valid/InValid. diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index ea3340f..4dc3723 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -106,6 +106,15 @@ namespace BEEV bool tseitin_are_decision_variables_flag; + // Available back-end SAT solvers. + enum SATSolvers + { + MINISAT_SOLVER =0, + SIMPLIFYING_MINISAT_SOLVER + }; + + enum SATSolvers solver_to_use; + //CONSTRUCTOR UserDefinedFlags() { @@ -192,6 +201,10 @@ namespace BEEV quick_statistics_flag=false; tseitin_are_decision_variables_flag=true; + + // use minisat by default. + solver_to_use = MINISAT_SOLVER; + } //End of constructor for UserDefinedFlags }; //End of struct UserDefinedFlags diff --git a/src/main/main.cpp b/src/main/main.cpp index bc70f3c..bc12946 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -47,7 +47,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; * step 5. Call SAT to determine if input is SAT or UNSAT ********************************************************************/ -typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF} OptionType; +typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType; int main(int argc, char ** argv) { char * infile; @@ -126,6 +126,12 @@ int main(int argc, char ** argv) { "-r : switch refinement off (optimizations are ON by default)\n"; helpstring += "-s : print function statistics\n"; + + #if !defined CRYPTOMINISAT && !defined CRYPTOMINISAT2 + helpstring += + "--simplifying-minisat : use simplifying-minisat rather than minisat\n"; + #endif + helpstring += "-t : print quick statistics\n"; helpstring += @@ -152,6 +158,8 @@ int main(int argc, char ** argv) { lookup.insert(make_pair("--print-back-dot",PRINT_BACK_DOT)); lookup.insert(make_pair("--output-CNF",OUTPUT_CNF)); lookup.insert(make_pair("--output-bench",OUTPUT_BENCH)); + lookup.insert(make_pair("--simplifying-minisat",USE_SIMPLIFYING_SOLVER)); + switch(lookup[argv[i]]) { @@ -183,6 +191,13 @@ int main(int argc, char ** argv) { bm->UserFlags.output_bench_flag = true; break; +#if !defined CRYPTOMINISAT && !defined CRYPTOMINISAT2 + case USE_SIMPLIFYING_SOLVER: + bm->UserFlags.solver_to_use = UserDefinedFlags::SIMPLIFYING_MINISAT_SOLVER; + break; +#endif + + default: fprintf(stderr,usage,prog); cout << helpstring; diff --git a/src/sat/Makefile b/src/sat/Makefile index 5ac03f3..010516e 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -1,10 +1,6 @@ .PHONY: core core: $(MAKE) -C core lib all - -.PHONY: simp -simp: - $(MAKE) -C core lib all $(MAKE) -C simp lib all .PHONY: cryptominisat @@ -15,7 +11,6 @@ cryptominisat: cryptominisat2: $(MAKE) -C cryptominisat2 lib all - .PHONY: clean clean: rm -rf *.o *~ libminisat.a diff --git a/src/sat/sat.h b/src/sat/sat.h index 7892b9e..bfd6c90 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -14,11 +14,7 @@ #ifdef CORE #include "core/Solver.h" #include "core/SolverTypes.h" -#endif - -#ifdef SIMP #include "simp/SimpSolver.h" -#include "core/SolverTypes.h" #endif #endif