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

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 98e43aaf05796d10831063f8f33f48ff671c3c8a..c4fe58fd7e921bd321abcf85b394ff3f9058cd03 100644 (file)
--- 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 27258b3c249b377a318705d421be2a90b39d43e7..201879eb0508a90254aee924ce65ad5f1cfb95b5 100644 (file)
--- 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 b300c3fb6e3cbb6f12307de164898485cf9bd129..cf241479cf7b7fd0b4b383ca45592fdcaf22a2d4 100644 (file)
--- 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)

diff --git a/src/smt/options b/src/smt/options
index 05a138f603c7b6154626b666106cfc0c82415140..458f42d6ac1b6f329e66902d76999b1f237c40a9 100644 (file)
--- a/src/smt/options
+++ b/src/smt/options
@@ -36,7 +36,7 @@ option produceAssignments produce-assignments --produce-assignments bool :defaul
 
 # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
 # is a mode in which the assertion list must be kept.  So it belongs here.
-common-option interactive interactive-mode --interactive bool :read-write
+common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
  force interactive mode
 
 option doITESimp --ite-simp bool :read-write

diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index 4edd91a8dfd93b89bff5e4f1807b255c9d44bc97..987d2e3c75ca10f2d6a5cc7dc018312ecbe69d52 100644 (file)
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -62,11 +62,15 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
     throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
   }
 
+  if(!value.isAtom()) {
+    throw OptionException("bad value for :" + key);
+  }
+
   string optionarg = value.getValue();
 
   ${smt_setoption_handlers}
 
-#line 70 "${template}"
+#line 74 "${template}"
 
   throw UnrecognizedOptionException(key);
 }
@@ -126,7 +130,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 
   ${smt_getoption_handlers}
 
-#line 130 "${template}"
+#line 134 "${template}"
 
   throw UnrecognizedOptionException(key);
 }