Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.

3 files changed, 27 insertions, 15 deletions

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 98e43aaf0..c4fe58fd7 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -5,7 +5,7 @@
  ** Major contributors:
  ** Minor contributors (to current version):
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -13,7 +13,7 @@
  **
  ** \brief SAT Solver.
  **
- ** Implementation of the minisat for cvc4.
+ ** Implementation of the minisat interface for cvc4.
  **/
 
 #include "prop/minisat/minisat.h"
@@ -111,8 +111,7 @@ void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
   Assert((unsigned)clause.size() == sat_clause.size());
 }
 
-void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
-{
+void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) {
 
   d_context = context;
 
@@ -125,20 +124,30 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory
   d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
                                       options::incrementalSolving() ||
                                       options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL );
+
+  d_statistics.init(d_minisat);
+}
+
+// Like initialize() above, but called just before each search when in
+// incremental mode
+void MinisatSatSolver::setupOptions() {
+  // Copy options from CVC4 options structure into minisat, as appropriate
+
   // Set up the verbosity
   d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;
 
   // Set up the random decision parameters
   d_minisat->random_var_freq = options::satRandomFreq();
-  d_minisat->random_seed = options::satRandomSeed();
+  // If 0, we use whatever we like (here, the Minisat default seed)
+  if(options::satRandomSeed() != 0) {
+    d_minisat->random_seed = double(options::satRandomSeed());
+  }
 
   // Give access to all possible options in the sat solver
   d_minisat->var_decay = options::satVarDecay();
   d_minisat->clause_decay = options::satClauseDecay();
   d_minisat->restart_first = options::satRestartFirst();
   d_minisat->restart_inc = options::satRestartInc();
-
-  d_statistics.init(d_minisat);
 }
 
 void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
@@ -153,6 +162,7 @@ SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool c
 
 SatValue MinisatSatSolver::solve(unsigned long& resource) {
   Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
+  setupOptions();
   if(resource == 0) {
     d_minisat->budgetOff();
   } else {
@@ -168,6 +178,7 @@ SatValue MinisatSatSolver::solve(unsigned long& resource) {
 }
 
 SatValue MinisatSatSolver::solve() {
+  setupOptions();
   d_minisat->budgetOff();
   return toSatLiteralValue(d_minisat->solve());
 }
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 27258b3c2..201879eb0 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -5,7 +5,7 @@
  ** Major contributors:
  ** Minor contributors (to current version):
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -13,7 +13,7 @@
  **
  ** \brief SAT Solver.
  **
- ** Implementation of the minisat for cvc4.
+ ** Implementation of the minisat interface for cvc4.
  **/
 
 #pragma once
@@ -36,6 +36,8 @@ class MinisatSatSolver : public DPLLSatSolverInterface {
   /** Context we will be using to synchronize the sat solver */
   context::Context* d_context;
 
+  void setupOptions();
+
 public:
 
   MinisatSatSolver();
@@ -96,11 +98,10 @@ public:
     Statistics();
     ~Statistics();
     void init(Minisat::SimpSolver* d_minisat);
-  };
+  };/* class MinisatSatSolver::Statistics */
   Statistics d_statistics;
 
-};
-
-} // prop namespace
-} // cvc4 namespace
+};/* class MinisatSatSolver */
 
+}/* CVC4::prop namespace */
+}/* CVC4 namespace */
diff --git a/src/prop/options b/src/prop/options
index b300c3fb6..cf241479c 100644
--- a/src/prop/options
+++ b/src/prop/options
@@ -10,7 +10,7 @@ option - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-in
 
 option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0)
  sets the frequency of random decisions in the sat solver (P=0.0 by default)
-option satRandomSeed random-seed --random-seed=S double :default 91648253 :read-write
+option satRandomSeed random-seed --random-seed=S uint32_t :default
  sets the random seed for the sat solver
 
 option satVarDecay double :default 0.95 :predicate less_equal(1.0) greater_equal(0.0)