diff options
| -rw-r--r-- | src/prop/sat.h | 7 | ||||
| -rw-r--r-- | src/util/options.cpp | 20 | ||||
| -rw-r--r-- | src/util/options.h | 13 |
3 files changed, 36 insertions, 4 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h index ea782234b..b80b0f705 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -270,10 +270,9 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine, // Setup the verbosity d_minisat->verbosity = (Options::current()->verbosity > 0) ? 1 : -1; - // No random choices - if(Debug.isOn("no_rnd_decisions")) { - d_minisat->random_var_freq = 0; - } + // Setup the random decision parameters + d_minisat->random_var_freq = Options::current()->satRandomFreq; + d_minisat->random_seed = Options::current()->satRandomSeed; d_statistics.init(d_minisat); } diff --git a/src/util/options.cpp b/src/util/options.cpp index 4bcc9a37d..88c8a2958 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -78,6 +78,8 @@ Options::Options() : earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT), incrementalSolving(false), rewriteArithEqualities(false), + satRandomFreq(0.0), + satRandomSeed(91648253), //Minisat's default value pivotRule(MINIMUM) { } @@ -110,6 +112,8 @@ static const string optionsDescription = "\ --produce-assignments support the get-assignment command\n\ --lazy-definition-expansion expand define-fun lazily\n\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ + --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ + --random-seed=S sets the random seed for the sat solver\n\ --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\ --incremental enable incremental solving\n"; @@ -166,6 +170,8 @@ enum OptionValue { EAGER_TYPE_CHECKING, INCREMENTAL, PIVOT_RULE, + RANDOM_FREQUENCY, + RANDOM_SEED, REWRITE_ARITHMETIC_EQUALITIES };/* enum OptionValue */ @@ -224,6 +230,8 @@ static struct option cmdlineOptions[] = { { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING }, { "incremental", no_argument, NULL, INCREMENTAL }, { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, + { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, + { "random-seed" , required_argument, NULL, RANDOM_SEED }, { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -426,6 +434,18 @@ throw(OptionException) { rewriteArithEqualities = true; break; + case RANDOM_SEED: + satRandomSeed = atof(optarg); + break; + + case RANDOM_FREQUENCY: + satRandomFreq = atof(optarg); + if(! (0.0 <= satRandomFreq && satRandomFreq <= 1.0)){ + throw OptionException(string("--random-freq: `") + + optarg + "' is not between 0.0 and 1.0."); + } + break; + case PIVOT_RULE: if(!strcmp(optarg, "min")) { pivotRule = MINIMUM; diff --git a/src/util/options.h b/src/util/options.h index efbd48900..dc0d231bd 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -131,6 +131,19 @@ struct CVC4_PUBLIC Options { /** Whether to rewrite equalities in arithmetic theory */ bool rewriteArithEqualities; + + /** + * Frequency for the sat solver to make random decisions. + * Should be between 0 and 1. + */ + double satRandomFreq; + + /** + * Seed for Minisat's random decision procedure. + * If this is 0, no random decisions will occur. + **/ + double satRandomSeed; + /** The pivot rule for arithmetic */ typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule; ArithPivotRule pivotRule; |