Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. Breaking an edge between the sat solver and command.h.

6 files changed, 18 insertions, 7 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 1cd32bee8..d54848d26 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -29,8 +29,8 @@
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
 #include "prop/theory_proxy.h"
+#include "smt/command.h"
 #include "smt/smt_engine_scope.h"
-#include "smt_util/command.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index f4489c4be..b7fb1603d 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -31,7 +31,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/minisat.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/theory_proxy.h"
-#include "smt_util/command.h"
 
 
 using namespace CVC4::prop;
@@ -479,15 +478,18 @@ void Solver::cancelUntil(int level) {
         for (int l = trail_lim.size() - level; l > 0; --l) {
           context->pop();
           if(Dump.isOn("state")) {
-            Dump("state") << PopCommand();
+            proxy->dumpStatePop();
           }
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
             vardata[x].trail_index = -1;
-            if ((phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) && (polarity[x] & 0x2) == 0)
+            if ((phase_saving > 1 ||
+                 ((phase_saving == 1) && c > trail_lim.last())
+                 ) && ((polarity[x] & 0x2) == 0)) {
               polarity[x] = sign(trail[c]);
+            }
             insertVarOrder(x);
         }
         qhead = trail_lim[level];
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index a239eba72..777fb1093 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -32,7 +32,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Heap.h"
 #include "prop/minisat/mtl/Vec.h"
 #include "prop/minisat/utils/Options.h"
-#include "smt_util/command.h"
 #include "theory/theory.h"
 
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 36d6408b5..583e9da18 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -36,7 +36,7 @@
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt_util/command.h"
+#include "smt/command.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
 #include "util/resource_manager.h"
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 5de97d0d8..63a09169f 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -23,9 +23,10 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "proof/cnf_proof.h"
+#include "smt/command.h"
+#include "smt/smt_statistics_registry.h"
 #include "smt_util/lemma_input_channel.h"
 #include "smt_util/lemma_output_channel.h"
-#include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "util/statistics_registry.h"
@@ -236,5 +237,11 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) {
   return d_decisionEngine->getPolarity(var);
 }
 
+void TheoryProxy::dumpStatePop() {
+  if(Dump.isOn("state")) {
+    Dump("state") << PopCommand();
+  }
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index acc242ab6..0e2b885d9 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -99,6 +99,9 @@ public:
 
   SatValue getDecisionPolarity(SatVariable var);
 
+  /** Shorthand for Dump("state") << PopCommand() */
+  void dumpStatePop();
+
  private:
   /** The prop engine we are using. */
   PropEngine* d_propEngine;