fixes to incremental simplification, cnf routines, other stuff in preparation of user push/pop in SAT solver

8 files changed, 109 insertions, 39 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 5b8e4c3f3..4e557d416 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -103,17 +103,22 @@ bool CnfStream::isTranslated(TNode n) const {
   return find != d_translationCache.end() && find->second.level >= 0;
 }
 
-bool CnfStream::hasLiteral(TNode n) const {
+bool CnfStream::hasEverHadLiteral(TNode n) const {
   TranslationCache::const_iterator find = d_translationCache.find(n);
   return find != d_translationCache.end();
 }
 
+bool CnfStream::currentlyHasLiteral(TNode n) const {
+  TranslationCache::const_iterator find = d_translationCache.find(n);
+  return find != d_translationCache.end() && (*find).second.level != -1;
+}
+
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
 
   // Get the literal for this node
   SatLiteral lit;
-  if (!hasLiteral(node)) {
+  if (!hasEverHadLiteral(node)) {
     // If no literal, well make one
     lit = variableToLiteral(d_satSolver->newVar(theoryLiteral));
     d_translationCache[node].literal = lit;
@@ -599,13 +604,16 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
-  if(hasLiteral(node)) {
+  /*
+  if(currentlyHasLiteral(node)) {
     Debug("cnf") << "==> fortunate literal detected!" << endl;
     ++d_fortunateLiterals;
     SatLiteral lit = getLiteral(node);
     //d_satSolver->renewVar(lit);
     assertClause(node, negated ? ~lit : lit);
+    return;
   }
+  */
 
   switch(node.getKind()) {
   case AND:
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index ecb0fd2fb..3ef636811 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -215,12 +215,16 @@ public:
   TNode getNode(const SatLiteral& literal);
 
   /**
-   * Returns true if the node has an assigned literal (it might not be translated).
-   * Caches the pair of the node and the literal corresponding to the
-   * translation.
+   * Returns true iff the node has an assigned literal (it might not be translated).
    * @param node the node
    */
-  bool hasLiteral(TNode node) const;
+  bool hasEverHadLiteral(TNode node) const;
+
+  /**
+   * Returns true iff the node has an assigned literal and it's translated.
+   * @param node the node
+   */
+  bool currentlyHasLiteral(TNode node) const;
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c8e4083b1..7b4155bde 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -167,7 +167,7 @@ Node PropEngine::getValue(TNode node) {
 }
 
 bool PropEngine::isSatLiteral(TNode node) {
-  return d_cnfStream->hasLiteral(node);
+  return d_cnfStream->hasEverHadLiteral(node);
 }
 
 bool PropEngine::hasValue(TNode node, bool& value) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 86d06520a..42b21b79a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -107,6 +107,9 @@ class SmtEnginePrivate {
   /** Learned literals */
   vector<Node> d_nonClausalLearnedLiterals;
 
+  /** A circuit propagator for non-clausal propositional deduction */
+  booleans::CircuitPropagator d_propagator;
+
   /** Assertions to push to sat */
   vector<Node> d_assertionsToCheck;
 
@@ -140,6 +143,8 @@ public:
 
   SmtEnginePrivate(SmtEngine& smt) :
     d_smt(smt),
+    d_nonClausalLearnedLiterals(),
+    d_propagator(smt.d_userContext, d_nonClausalLearnedLiterals, true, true),
     d_topLevelSubstitutions(smt.d_userContext) {
   }
 
@@ -244,6 +249,8 @@ SmtEngine::~SmtEngine() {
   StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
   StatisticsRegistry::unregisterStat(&d_staticLearningTime);
 
+  // Deletion order error: circuit propagator has some unsafe TNodes ?!
+  // delete d_private;
   delete d_userContext;
 
   delete d_theoryEngine;
@@ -559,7 +566,7 @@ void SmtEnginePrivate::staticLearning() {
 
 void SmtEnginePrivate::nonClausalSimplify() {
 
-  TimerStat::CodeTimer nonclauselTimer(d_smt.d_nonclausalSimplificationTime);
+  TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime);
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
 
@@ -571,19 +578,16 @@ void SmtEnginePrivate::nonClausalSimplify() {
       theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
   }
 
-  d_nonClausalLearnedLiterals.clear();
-  booleans::CircuitPropagator propagator(d_nonClausalLearnedLiterals, true, true);
-
   // Assert all the assertions to the propagator
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "asserting to propagator" << endl;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    propagator.assert(d_assertionsToPreprocess[i]);
+    d_propagator.assert(d_assertionsToPreprocess[i]);
   }
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "propagating" << endl;
-  if (propagator.propagate()) {
+  if (d_propagator.propagate()) {
     // If in conflict, just return false
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "conflict in non-clausal propagation" << endl;
@@ -1082,22 +1086,25 @@ void SmtEngine::pop() {
                        << d_userContext->getLevel() << endl;
   // FIXME: should we reset d_status here?
   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
+  // Still, we want the right exit status after any final sequence
+  // of pops... hm.
 }
 
-void SmtEngine::internalPop() {
-  Trace("smt") << "internalPop()" << endl;
-  d_propEngine->pop();
-  d_userContext->pop();
+void SmtEngine::internalPush() {
+  Trace("smt") << "SmtEngine::internalPush()" << endl;
+  if(Options::current()->incrementalSolving) {
+    d_private->processAssertions();
+    d_userContext->push();
+    d_propEngine->push();
+  }
 }
 
-void SmtEngine::internalPush() {
-  Trace("smt") << "internalPush()" << endl;
-  // TODO: this is the right thing to do, but needs serious thinking
-  // to keep completeness
-  //
-  // d_private->processAssertions();
-  d_userContext->push();
-  d_propEngine->push();
+void SmtEngine::internalPop() {
+  Trace("smt") << "SmtEngine::internalPop()" << endl;
+  if(Options::current()->incrementalSolving) {
+    d_propEngine->pop();
+    d_userContext->pop();
+  }
 }
 
 StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 7a5f39056..f5036bed7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -137,7 +137,7 @@ class CVC4_PUBLIC SmtEngine {
 
   /**
    * Whether or not a query() or checkSat() has already been made through
-   * this SmtEngine.  If true, and d_incrementalSolving is false, then
+   * this SmtEngine.  If true, and incrementalSolving is false, then
    * attempting an additional query() or checkSat() will fail with a
    * ModalException.
    */
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 9593f7735..e1e3073ce 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -28,6 +28,9 @@
 #include "context/context.h"
 #include "util/hash.h"
 #include "expr/node.h"
+#include "context/cdset.h"
+#include "context/cdmap.h"
+#include "context/cdo.h"
 
 namespace CVC4 {
 namespace theory {
@@ -72,20 +75,50 @@ private:
   /** The propagation queue */
   std::vector<TNode> d_propagationQueue;
 
+  /** A context-notify object that clears out stale data. */
+  template <class T>
+  class DataClearer : context::ContextNotifyObj {
+    T& d_data;
+  public:
+    DataClearer(context::Context* context, T& data) :
+      context::ContextNotifyObj(context),
+      d_data(data) {
+    }
+
+    void notify() {
+      Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data "
+                            << "(size was " << d_data.size() << ")" << std::endl;
+      d_data.clear();
+    }
+  };/* class DataClearer<T> */
+
+  /**
+   * We have a propagation queue "clearer" object for when the user
+   * context pops.  Normally the propagation queue should be empty,
+   * but this keeps us safe in case there's still some rubbish around
+   * on the queue.
+   */
+  DataClearer< std::vector<TNode> > d_propagationQueueClearer;
+
   /** Are we in conflict */
-  bool d_conflict;
+  context::CDO<bool> d_conflict;
 
   /** Map of substitutions */
   std::vector<Node>& d_learnedLiterals;
 
+  /**
+   * Similar data clearer for learned literals.
+   */
+  DataClearer< std::vector<Node> > d_learnedLiteralClearer;
+
   /** Nodes that have been attached already (computed forward edges for) */
   // All the nodes we've visited so far
-  std::hash_set<TNode, TNodeHashFunction> d_seen;
+  context::CDSet<TNode, TNodeHashFunction> d_seen;
 
   /**
    * Assignment status of each node.
    */
-  typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
+  typedef context::CDMap<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap;
   AssignmentMap d_state;
 
   /**
@@ -93,7 +126,7 @@ private:
    */
   void assignAndEnqueue(TNode n, bool value) {
 
-    Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
+    Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl;
 
     if (n.getKind() == kind::CONST_BOOLEAN) {
       // Assigning a constant to the opposite value is dumb
@@ -136,8 +169,9 @@ private:
 
   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
   bool getAssignment(TNode n) const {
-    Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED);
-    return d_state.find(n)->second == ASSIGNED_TO_TRUE;
+    AssignmentMap::iterator i = d_state.find(n);
+    Assert(i != d_state.end() && (*i).second != UNASSIGNED);
+    return (*i).second == ASSIGNED_TO_TRUE;
   }
 
   /** Predicate for use in STL functions. */
@@ -186,17 +220,25 @@ private:
   void propagateBackward(TNode parent, bool assignment);
 
   /** Whether to perform forward propagation */
-  bool d_forwardPropagation;
+  const bool d_forwardPropagation;
+
   /** Whether to perform backward propagation */
-  bool d_backwardPropagation;
+  const bool d_backwardPropagation;
 
 public:
   /**
-   * Construct a new CircuitPropagator with the given atoms and backEdges.
+   * Construct a new CircuitPropagator.
    */
-  CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) :
-    d_conflict(false),
+  CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals,
+                    bool enableForward = true, bool enableBackward = true) :
+    d_backEdges(),
+    d_propagationQueue(),
+    d_propagationQueueClearer(context, d_propagationQueue),
+    d_conflict(context, false),
     d_learnedLiterals(outLearnedLiterals),
+    d_learnedLiteralClearer(context, outLearnedLiterals),
+    d_seen(context),
+    d_state(context),
     d_forwardPropagation(enableForward),
     d_backwardPropagation(enableBackward) {
   }
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index fb0abfe25..948731057 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -74,7 +74,8 @@ CVC_TESTS = \
 	wiki.18.cvc \
 	wiki.19.cvc \
 	wiki.20.cvc \
-	wiki.21.cvc
+	wiki.21.cvc \
+	simplification_bug3.cvc
 
 # Regression tests derived from bug reports
 BUG_TESTS = \
diff --git a/test/regress/regress0/simplification_bug3.cvc b/test/regress/regress0/simplification_bug3.cvc
new file mode 100644
index 000000000..26efad5b6
--- /dev/null
+++ b/test/regress/regress0/simplification_bug3.cvc
@@ -0,0 +1,8 @@
+% COMMAND-LINE: --simplification=incremental
+x, y: BOOLEAN;
+ASSERT x OR y;
+ASSERT NOT x;
+ASSERT NOT y;
+% EXPECT: unsat
+CHECKSAT;
+% EXIT: 20