From: Tim King <taking@cs.nyu.edu>
Date: Tue, 5 Apr 2011 15:58:59 +0000 (+0000)
Subject: Added options for setting the random decision frequency and random seed for the sat... 
X-Git-Tag: cvc5-1.0.0~8613
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ab9caadb0d56e7788c879b82944ad4a2485135a;p=cvc5.git

Added options for setting the random decision frequency and random seed for the sat solver.  Also added command line options for setting both.
---

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;