From 01e3d838982658349f429063834379b7cda43dbc Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 11 Mar 2014 15:07:38 -0400
Subject: Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.

---
 src/prop/minisat/minisat.cpp | 25 ++++++++++++++++++-------
 src/prop/minisat/minisat.h   | 15 ++++++++-------
 2 files changed, 26 insertions(+), 14 deletions(-)

(limited to 'src/prop/minisat')

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 */
-- 
cgit v1.2.3