From 64d530e5b9096e66398f92d93cf7bc4268df0e70 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 3 Feb 2010 22:20:25 +0000
Subject: Addressed many of the concerns of bug 10 (build system code review).
 Some parts split into other bugs: 19, 20, 21.

Addressed concerns of bug 11 (util package code review).

Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers

Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main().  Silenced MiniSat when
verbosity is not requested.
---
 src/prop/minisat/core/Solver.C |  3 ++-
 src/prop/prop_engine.cpp       | 13 ++++++++++---
 src/prop/prop_engine.h         | 21 +++++++++++----------
 3 files changed, 23 insertions(+), 14 deletions(-)

(limited to 'src/prop')

diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C
index 4ea33e101..e99870654 100644
--- a/src/prop/minisat/core/Solver.C
+++ b/src/prop/minisat/core/Solver.C
@@ -724,7 +724,8 @@ void Solver::verifyModel()
 
     assert(!failed);
 
-    reportf("Verified %d original clauses.\n", clauses.size());
+    if(verbosity >= 1)
+        reportf("Verified %d original clauses.\n", clauses.size());
 }
 
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index b4df32f0f..3455b845e 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -22,6 +22,8 @@
 #include "prop/minisat/core/SolverTypes.h"
 #include "util/Assert.h"
 #include "util/output.h"
+#include "util/options.h"
+#include "util/result.h"
 
 #include <utility>
 #include <map>
@@ -31,7 +33,10 @@ using namespace std;
 
 namespace CVC4 {
 
-PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
+PropEngine::PropEngine(const Options* opts,
+                       DecisionEngine& de,
+                       TheoryEngine& te) :
+  d_opts(opts),
   d_de(de), 
   d_te(te), 
   d_restartMayBeNeeded(false){
@@ -82,11 +87,11 @@ void PropEngine::restart(){
   }
 }
 
-void PropEngine::solve() {
+Result PropEngine::solve() {
   if(d_restartMayBeNeeded)
     restart();
 
-  d_sat->verbosity = 1;
+  d_sat->verbosity = (d_opts->verbosity > 0) ? 1 : -1;
   bool result = d_sat->solve();
 
   if(!result){
@@ -94,6 +99,8 @@ void PropEngine::solve() {
   }
 
   Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
+
+  return Result(result ? Result::SAT : Result::UNSAT);
 }
 
 }/* CVC4 namespace */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 9f5f9dac1..181c0288e 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -23,6 +23,7 @@
 #include "theory/theory_engine.h"
 #include "prop/minisat/simp/SimpSolver.h"
 #include "prop/minisat/core/SolverTypes.h"
+#include "util/result.h"
 
 #include <map>
 #include "prop/cnf_stream.h"
@@ -31,6 +32,8 @@ namespace CVC4 {
   namespace prop {
     class CnfStream;
   }
+
+  class Options;
 }
 
 namespace CVC4 {
@@ -40,20 +43,16 @@ namespace CVC4 {
 // propositional solver, DPLL or otherwise.
 
 class PropEngine {
+  const Options *d_opts;
   DecisionEngine &d_de;
   TheoryEngine &d_te;
 
   friend class CVC4::prop::CnfStream;
   
-  /* Morgan: I added these back.
-   * Why did you push these into solve()?
-   * I am guessing this is for either a technical reason I'm not seeing,
-   * or that you wanted to have a clean restart everytime solve() was called
-   * and to start from scratch everytime. (Avoid push/pop problems?)
-   * Is this right?
+  /**
+   * The SAT solver.
    */
-  CVC4::prop::minisat::Solver * d_sat;
-
+  CVC4::prop::minisat::Solver* d_sat;
 
   std::map<Node, CVC4::prop::minisat::Lit> d_atom2lit;
   std::map<CVC4::prop::minisat::Lit, Node> d_lit2atom;
@@ -101,7 +100,9 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&);
+  CVC4_PUBLIC PropEngine(const CVC4::Options* opts,
+                         CVC4::DecisionEngine&,
+                         CVC4::TheoryEngine&);
   CVC4_PUBLIC ~PropEngine();
 
   /**
@@ -115,7 +116,7 @@ public:
    * and invokes the sat solver for a satisfying assignment.
    * TODO: what does well-formed mean here?
    */
-  void solve();
+  Result solve();
 
 };/* class PropEngine */
 
-- 
cgit v1.2.3