merge from symmetry branch

2 files changed, 31 insertions, 5 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8e98f32c0..0c4f00875 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -240,8 +240,18 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
     if (ps.size() == 0)
         return ok = false;
     else if (ps.size() == 1){
-        assert(type != CLAUSE_LEMMA);
-        assert(value(ps[0]) == l_Undef);
+        if(in_solve) {
+          assert(type != CLAUSE_LEMMA);
+          assert(value(ps[0]) == l_Undef);
+        } else {
+          // [MGD] at "pre-solve" time we allow unit T-lemmas
+          if(value(ps[0]) == l_True) {
+            // this unit T-lemma is extraneous (perhaps it was
+            // discovered twice at presolve time)
+            return true;
+          }
+          assert(value(ps[0]) == l_Undef);
+        }
         uncheckedEnqueue(ps[0]);
         return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
     }else{
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index cbec9faea..4c9b66020 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -16,9 +16,9 @@
  ** Implementation of the propositional engine of CVC4.
  **/
 
-#include "cnf_stream.h"
-#include "prop_engine.h"
-#include "sat.h"
+#include "prop/cnf_stream.h"
+#include "prop/prop_engine.h"
+#include "prop/sat.h"
 
 #include "theory/theory_engine.h"
 #include "theory/registrar.h"
@@ -26,6 +26,8 @@
 #include "util/options.h"
 #include "util/output.h"
 #include "util/result.h"
+#include "expr/expr.h"
+#include "expr/command.h"
 
 #include <utility>
 #include <map>
@@ -88,6 +90,16 @@ void PropEngine::assertLemma(TNode node) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
+  if(Options::current()->preprocessOnly) {
+    if(Message.isOn()) {
+      // If "preprocess only" mode is in effect, the lemmas we get
+      // here are due to theory reasoning during preprocessing.  So
+      // push the lemma to the Message() stream.
+      expr::ExprSetDepth::Scope sdScope(Message.getStream(), -1);
+      Message() << AssertCommand(BoolExpr(node.toExpr())) << endl;
+    }
+  }
+
   //TODO This comment is now false
   // Assert as removable
   d_cnfStream->convertAndAssert(node, true, false);
@@ -124,6 +136,10 @@ Result PropEngine::checkSat() {
   // TODO This currently ignores conflicts (a dangerous practice).
   d_theoryEngine->presolve();
 
+  if(Options::current()->preprocessOnly) {
+    return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+  }
+
   // Check the problem
   bool result = d_satSolver->solve();