From: trevor_hansen Date: Tue, 10 Jan 2012 04:59:09 +0000 (+0000) Subject: Improvement. Ability to give a random number to the SAT solver. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=55f42e76983a9635aafa73437b03877591f6ff45;p=francis%2Fstp.git Improvement. Ability to give a random number to the SAT solver. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1491 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 13fbad6..6836144 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -72,6 +72,11 @@ namespace BEEV { NewSolver.setVerbosity(1); } + if(bm->UserFlags.random_seed_flag) + { + NewSolver.setSeed(bm->UserFlags.random_seed); + } + SOLVER_RETURN_TYPE result; result = TopLevelSTPAux(NewSolver, original_input); diff --git a/src/main/main.cpp b/src/main/main.cpp index d260785..ac08bb2 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -78,7 +78,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_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT, DISABLE_EQUALITY} OptionType; +typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT, DISABLE_CBITP,EXIT_AFTER_CNF,USE_CRYPTOMINISAT_SOLVER,USE_MINISAT_SOLVER, DISABLE_SIMPLIFICATIONS, OLDSTYLE_REFINEMENT, DISABLE_EQUALITY, RANDOM_SEED} OptionType; int main(int argc, char ** argv) { @@ -153,6 +153,7 @@ int main(int argc, char ** argv) { "-g : timeout (seconds until STP gives up)\n" "-h : help\n" "-i : Randomize STP's satisfiable output. Random_seed is an integer >= 0\n" + "--random-seed : Generate a random number for the SAT solver.\n" "-p : print counterexample\n" "-s : print function statistics\n" "-t : print quick statistics\n" @@ -190,6 +191,7 @@ int main(int argc, char ** argv) { lookup.insert(make_pair(tolower("--disable-simplify"),DISABLE_SIMPLIFICATIONS)); lookup.insert(make_pair(tolower("--oldstyle-refinement"),OLDSTYLE_REFINEMENT)); lookup.insert(make_pair(tolower("--disable-equality"),DISABLE_EQUALITY)); + lookup.insert(make_pair(tolower("--random-seed"),RANDOM_SEED)); if (!strncmp(argv[i],"--config_",strlen("--config_"))) @@ -284,6 +286,13 @@ int main(int argc, char ** argv) { case DISABLE_EQUALITY: bm->UserFlags.propagate_equalities = false; break; + case RANDOM_SEED: + { + srand(time(NULL)); + bm->UserFlags.random_seed_flag = true; + bm->UserFlags.random_seed = rand(); + } + break; default: fprintf(stderr,usage,prog); diff --git a/src/sat/CryptoMinisat.h b/src/sat/CryptoMinisat.h index c7832e0..4a45c97 100644 --- a/src/sat/CryptoMinisat.h +++ b/src/sat/CryptoMinisat.h @@ -1,8 +1,8 @@ /* - * Wraps around CORE minisat. + * Wraps around Cryptominisat minisat. */ -#ifndef MINISATCORE_H_ -#define MINIASTCORE_H_ +#ifndef CRYPTOMINISAT_H_ +#define CRYPTOMINISAT_H_ #include "SATSolver.h" diff --git a/src/sat/MinisatCore.cpp b/src/sat/MinisatCore.cpp index 9733bdf..c655fa2 100644 --- a/src/sat/MinisatCore.cpp +++ b/src/sat/MinisatCore.cpp @@ -63,6 +63,13 @@ namespace BEEV s->verbosity = v; } + template + void MinisatCore::setSeed(int i) + { + s->random_seed = i; + } + + template int MinisatCore::nVars() {return s->nVars();} diff --git a/src/sat/MinisatCore.h b/src/sat/MinisatCore.h index 58e89ba..0f4d02e 100644 --- a/src/sat/MinisatCore.h +++ b/src/sat/MinisatCore.h @@ -46,11 +46,11 @@ namespace BEEV void printStats(); + virtual void setSeed(int i); + virtual lbool true_literal() {return ((uint8_t)0);} virtual lbool false_literal() {return ((uint8_t)1);} virtual lbool undef_literal() {return ((uint8_t)2);} - - }; } ; diff --git a/src/sat/MinisatCore_prop.cpp b/src/sat/MinisatCore_prop.cpp index 1a01b7f..4dacfb7 100644 --- a/src/sat/MinisatCore_prop.cpp +++ b/src/sat/MinisatCore_prop.cpp @@ -89,5 +89,11 @@ namespace BEEV printf("CPU time : %g s\n", cpu_time); } + template + void MinisatCore_prop::setSeed(int i) + { + s->random_seed = i; + } + template class MinisatCore_prop; }; diff --git a/src/sat/MinisatCore_prop.h b/src/sat/MinisatCore_prop.h index 9145bb3..5dc3688 100644 --- a/src/sat/MinisatCore_prop.h +++ b/src/sat/MinisatCore_prop.h @@ -1,8 +1,8 @@ /* - * Wraps around CORE minisat. + * Wraps around minisat with array propagators */ -#ifndef MINISATCORE_H_ -#define MINIASTCORE_H_ +#ifndef MINISATCORE_PROP_H_ +#define MINIASTCORE_PROP_H_ #include "SATSolver.h" @@ -53,7 +53,7 @@ namespace BEEV virtual lbool false_literal() {return ((uint8_t)1);} virtual lbool undef_literal() {return ((uint8_t)2);} - + virtual void setSeed(int i); }; } ; diff --git a/src/sat/SATSolver.h b/src/sat/SATSolver.h index 38839df..af0df23 100644 --- a/src/sat/SATSolver.h +++ b/src/sat/SATSolver.h @@ -56,7 +56,10 @@ namespace BEEV virtual void printStats() = 0; virtual void setSeed(int i) - {} + { + std::cerr << "Setting the random seen is not implemented for this solver" << std::endl; + exit(1); + } virtual int setVerbosity(int v) =0; diff --git a/src/sat/SimplifyingMinisat.cpp b/src/sat/SimplifyingMinisat.cpp index 7bd5295..3794445 100644 --- a/src/sat/SimplifyingMinisat.cpp +++ b/src/sat/SimplifyingMinisat.cpp @@ -52,6 +52,11 @@ namespace BEEV s->verbosity = v; } + void SimplifyingMinisat::setSeed(int i) + { + s->random_seed = i; + } + Minisat::Var SimplifyingMinisat::newVar() { diff --git a/src/sat/SimplifyingMinisat.h b/src/sat/SimplifyingMinisat.h index 314b188..7c746e5 100644 --- a/src/sat/SimplifyingMinisat.h +++ b/src/sat/SimplifyingMinisat.h @@ -1,8 +1,8 @@ /* * Wraps around Simplifying minisat. */ -#ifndef CORE_H_ -#define CORE_H_ +#ifndef SIMPLIFYINGMINISAT_H_ +#define SIMPLIFYINGMINISAT_H_ #include "SATSolver.h" @@ -44,6 +44,8 @@ namespace BEEV void printStats(); + virtual void setSeed(int i); + virtual lbool true_literal() {return ((uint8_t)0);} virtual lbool false_literal() {return ((uint8_t)1);} virtual lbool undef_literal() {return ((uint8_t)2);}