Added OutputChannel::propagateAsDecision() functionality, allowing a theory

to request a decision on a literal.  All these theory requests are kept in a
context-dependent queue and serviced in order when the SAT solver goes to make a
decision.  Requests that don't have a SAT literal give an assert-fail.  Requests
for literals that already have an assignment are silently ignored.

Since the queue is CD, requests can actually be serviced more than once (e.g., if
a request is made at DL 5, but not serviced until DL 10, and later, a conflict
backtracks to level 7, the request may be serviced again).

Performance impact: none to negligible for theories that don't use it
  See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index e1a8ded8eddfe299083d905e51c20c8eb854ff67..cdab47163caa61d2f221f873d6b5a55b5a05011f 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -355,13 +355,27 @@ void Solver::popTrail() {
 
 Lit Solver::pickBranchLit()
 {
+    Lit nextLit;
+
 #ifdef CVC4_REPLAY
-    Lit nextLit = proxy->getNextReplayDecision();
+    nextLit = proxy->getNextReplayDecision();
     if (nextLit != lit_Undef) {
       return nextLit;
     }
 #endif /* CVC4_REPLAY */
 
+    // Theory requests
+    nextLit = proxy->getNextDecisionRequest();
+    while (nextLit != lit_Undef) {
+      if(value(var(nextLit)) == l_Undef) {
+        Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
+        return nextLit;
+      } else {
+        Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
+      }
+      nextLit = proxy->getNextDecisionRequest();
+    }
+
     Var next = var_Undef;
 
     // Random decision:
@@ -699,6 +713,7 @@ void Solver::propagateTheory() {
   std::vector<Lit> propagatedLiterals;
   proxy->theoryPropagate(propagatedLiterals);
   int oldTrailSize = trail.size();
+  Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
   for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) {
     Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
     // multiple theories can propagate the same literal
@@ -707,6 +722,7 @@ void Solver::propagateTheory() {
       uncheckedEnqueue(p, CRef_Lazy);
     } else {
       // but we check that this is the case and that they agree
+      Debug("minisat") << "trail_index(var(p)) == " << trail_index(var(p)) << std::endl;
       Assert(trail_index(var(p)) >= oldTrailSize);
       Assert(value(p) == lbool(!sign(p)));
     }

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 7df7535dd40c6dfde40ada4e97448bfa8b1993e7..559467922155dcbfd19daadbba9bf06d9ac6c979 100644 (file)
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -71,6 +71,11 @@ void SatSolver::enqueueTheoryLiteral(const SatLiteral& l) {
   d_theoryEngine->assertFact(literalNode);
 }
 
+SatLiteral SatSolver::getNextDecisionRequest() {
+  TNode n = d_theoryEngine->getNextDecisionRequest();
+  return n.isNull() ? Minisat::lit_Undef : d_cnfStream->getLiteral(n);
+}
+
 bool SatSolver::theoryNeedCheck() const {
   return d_theoryEngine->needCheck();
 }

diff --git a/src/prop/sat.h b/src/prop/sat.h
index e86443827c9def92bd91775dc2feeea7cb10e745..3f3166c140ca468fb9c69dbd746ea43c219f0f25 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -236,6 +236,8 @@ public:
 
   void enqueueTheoryLiteral(const SatLiteral& l);
 
+  SatLiteral getNextDecisionRequest();
+
   bool theoryNeedCheck() const;
 
   void setCnfStream(CnfStream* cnfStream);

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 0e47cd7f2c37834cca624e11363b9cddb09a502f..71bbefb6a6b3b7a089eae4bd19ec3ae6f0d03f12 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -106,6 +106,24 @@ public:
    */
   virtual void propagate(TNode n) throw(AssertionException) = 0;
 
+  /**
+   * Request that the core make a decision on this atom.  The decision
+   * will be "as soon as possible," but due to other propagation and
+   * conflict-detection work going on internally, the request is queued
+   * up and may be behind other such requests.  The request will be
+   * silently dropped if the atom has a definite value at the point the
+   * request would be serviced.  This request is also context-dependent
+   * on the search context, meaning that it will be dropped completely
+   * if a conflict is found before it is serviced.  Each request will only
+   * be serviced a single time, even though the atom may become undefined
+   * due to backtracking.
+   *
+   * @param atom the atom to decide upon (or the negation of an
+   * atom---the decision will be in the phase provided); must be
+   * associated to a SAT literal.
+   */
+  virtual void propagateAsDecision(TNode n) throw(AssertionException) = 0;
+
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
    * been detected.  (This requests a split.)

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 75c64654d5f0da7eb12d76501ce84c80a4f64a89..c4a8dc59119dc2599edcd10f35c6f84807f9e91b 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -55,6 +55,8 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_logic(""),
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
+  d_decisionRequests(context),
+  d_decisionRequestsIndex(context, 0),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms)
 {
@@ -665,13 +667,22 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   }
 }
 
+void TheoryEngine::propagateAsDecision(TNode literal, theory::TheoryId theory) {
+  Debug("theory") << "EngineOutputChannel::propagateAsDecision(" << literal << ", " << theory << ")" << std::endl;
+
+  d_propEngine->checkTime();
+
+  Assert(d_propEngine->isSatLiteral(literal.getKind() == kind::NOT ? literal[0] : literal), "OutputChannel::propagateAsDecision() requires a SAT literal (or negation of one)");
+
+  d_decisionRequests.push_back(literal);
+}
+
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   Assert(a.getType() == b.getType());
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
-Node TheoryEngine::getExplanation(TNode node)
-{
+Node TheoryEngine::getExplanation(TNode node) {
   Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl;
 
   TNode atom = node.getKind() == kind::NOT ? node[0] : node;

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6385d1467f101c78f6beb3a29cccd967ab023620..be1c3abafd830358591844ed52c12a52e3487063 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -57,14 +57,14 @@ struct NodeTheoryPair {
   bool operator == (const NodeTheoryPair& pair) const {
     return node == pair.node && theory == pair.theory;
   }
-};
+};/* struct NodeTheoryPair */
 
 struct NodeTheoryPairHashFunction {
   NodeHashFunction hashFunction;
   size_t operator()(const NodeTheoryPair& pair) const {
     return hashFunction(pair.node)*0x9e3779b9 + pair.theory;
   }
-};
+};/* struct NodeTheoryPairHashFunction */
 
 /**
  * This is essentially an abstraction for a collection of theories.  A
@@ -128,7 +128,9 @@ class TheoryEngine {
    */
   class Statistics {
 
-    static std::string mkName(std::string prefix, theory::TheoryId theory, std::string suffix) {
+    static std::string mkName(std::string prefix,
+                              theory::TheoryId theory,
+                              std::string suffix) {
       std::stringstream ss;
       ss << prefix << theory << suffix;
       return ss.str();
@@ -136,22 +138,25 @@ class TheoryEngine {
 
   public:
 
-    IntStat conflicts, propagations, lemmas;
+    IntStat conflicts, propagations, lemmas, propagationsAsDecisions;
 
     Statistics(theory::TheoryId theory):
       conflicts(mkName("theory<", theory, ">::conflicts"), 0),
       propagations(mkName("theory<", theory, ">::propagations"), 0),
-      lemmas(mkName("theory<", theory, ">::lemmas"), 0)
+      lemmas(mkName("theory<", theory, ">::lemmas"), 0),
+      propagationsAsDecisions(mkName("theory<", theory, ">::propagationsAsDecisions"), 0)
     {
       StatisticsRegistry::registerStat(&conflicts);
       StatisticsRegistry::registerStat(&propagations);
       StatisticsRegistry::registerStat(&lemmas);
+      StatisticsRegistry::registerStat(&propagationsAsDecisions);
     }
 
     ~Statistics() {
       StatisticsRegistry::unregisterStat(&conflicts);
       StatisticsRegistry::unregisterStat(&propagations);
       StatisticsRegistry::unregisterStat(&lemmas);
+      StatisticsRegistry::unregisterStat(&propagationsAsDecisions);
     }
   };/* class TheoryEngine::Statistics */
 
@@ -202,6 +207,13 @@ class TheoryEngine {
       d_engine->propagate(literal, d_theory);
     }
 
+    void propagateAsDecision(TNode literal) throw(AssertionException) {
+      Trace("theory") << "EngineOutputChannel<" << d_theory << ">::propagateAsDecision(" << literal << ")" << std::endl;
+      ++ d_statistics.propagationsAsDecisions;
+      d_engine->d_outputChannelUsed = true;
+      d_engine->propagateAsDecision(literal, d_theory);
+    }
+
     theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
       Trace("theory") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
@@ -217,7 +229,7 @@ class TheoryEngine {
       d_engine->spendResource();
     }
 
-  };/* class EngineOutputChannel */
+  };/* class TheoryEngine::EngineOutputChannel */
 
   /**
    * Output channels for individual theories.
@@ -235,8 +247,9 @@ class TheoryEngine {
   context::CDO<bool> d_sharedTermsExist;
 
   /**
-   * Explain the equality literals and push all the explaining literals into the builder. All
-   * the non-equality literals are pushed to the builder.
+   * Explain the equality literals and push all the explaining literals
+   * into the builder. All the non-equality literals are pushed to the
+   * builder.
    */
   void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder);
 
@@ -288,18 +301,18 @@ class TheoryEngine {
     NodeTheoryPair toAssert;
     /** This is the node/theory pair that we will use to explain it */
     NodeTheoryPair toExplain;
-    
+
     SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory)
     : toAssert(assertion, receivingTheory),
       toExplain(original, sendingTheory)
     { }
-  };
-  
+  };/* struct SharedEquality */
+
   /**
-   * Map from equalities asserted to a theory, to the theory that can explain them. 
+   * Map from equalities asserted to a theory, to the theory that can explain them.
    */
   typedef context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap;
-  
+
   /**
    * A map from asserted facts to where they came from (for explanations).
    */
@@ -316,7 +329,7 @@ class TheoryEngine {
   /**
    * Literals that are propagated by the theory. Note that these are TNodes.
    * The theory can only propagate nodes that have an assigned literal in the
-   * sat solver and are hence referenced in the SAT solver.
+   * SAT solver and are hence referenced in the SAT solver.
    */
   context::CDList<TNode> d_propagatedLiterals;
 
@@ -330,6 +343,19 @@ class TheoryEngine {
    */
   std::vector<SharedEquality> d_propagatedEqualities;
 
+  /**
+   * Decisions that are requested via propagateAsDecision().  The theory
+   * can only request decisions on nodes that have an assigned litearl in
+   * the SAT solver and are hence referenced in the SAT solver (making the
+   * use of TNode safe).
+   */
+  context::CDList<TNode> d_decisionRequests;
+
+  /**
+   * The index of the next decision requested by a theory.
+   */
+  context::CDO<unsigned> d_decisionRequestsIndex;
+
   /**
    * Called by the output channel to propagate literals and facts
    */
@@ -341,6 +367,12 @@ class TheoryEngine {
    */
   void propagate(theory::Theory::Effort effort);
 
+  /**
+   * Called by the output channel to request decisions "as soon as
+   * possible."
+   */
+  void propagateAsDecision(TNode literal, theory::TheoryId theory);
+
   /**
    * A variable to mark if we added any lemmas.
    */
@@ -541,6 +573,19 @@ public:
     }
   }
 
+  TNode getNextDecisionRequest() {
+    if(d_decisionRequestsIndex < d_decisionRequests.size()) {
+      TNode req = d_decisionRequests[d_decisionRequestsIndex];
+      Debug("propagateAsDecision") << "TheoryEngine requesting decision["
+                                   << d_decisionRequestsIndex << "]: "
+                                   << req << std::endl;
+      d_decisionRequestsIndex = d_decisionRequestsIndex + 1;
+      return req;
+    } else {
+      return TNode::null();
+    }
+  }
+
   bool properConflict(TNode conflict) const;
   bool properPropagation(TNode lit) const;
   bool properExplanation(TNode node, TNode expl) const;
@@ -572,8 +617,8 @@ public:
   }
 
   /**
-   * Returns the equality status of the two terms, from the theory that owns the domain type.
-   * The types of a and b must be the same.
+   * Returns the equality status of the two terms, from the theory
+   * that owns the domain type.  The types of a and b must be the same.
    */
   theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
 
@@ -583,7 +628,7 @@ private:
   PreRegisterVisitor d_preRegistrationVisitor;
 
   /** Visitor for collecting shared terms */
-  SharedTermsVisitor d_sharedTermsVisitor; 
+  SharedTermsVisitor d_sharedTermsVisitor;
 
 };/* class TheoryEngine */
 

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 96bd02b5a199ac261dda92a4810e4a81ad6e92d0..aaf47425bfa4167ff2e007a09c49afa414e8bcdd 100644 (file)
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -41,6 +41,7 @@ namespace theory {
 enum OutputChannelCallType {
   CONFLICT,
   PROPAGATE,
+  PROPAGATE_AS_DECISION,
   AUG_LEMMA,
   LEMMA,
   EXPLANATION
@@ -52,6 +53,7 @@ inline std::ostream& operator<<(std::ostream& out, theory::OutputChannelCallType
   switch(type) {
   case theory::CONFLICT: return out << "CONFLICT";
   case theory::PROPAGATE: return out << "PROPAGATE";
+  case theory::PROPAGATE_AS_DECISION: return out << "PROPAGATE_AS_DECISION";
   case theory::AUG_LEMMA: return out << "AUG_LEMMA";
   case theory::LEMMA: return out << "LEMMA";
   case theory::EXPLANATION: return out << "EXPLANATION";
@@ -81,6 +83,11 @@ public:
     push(PROPAGATE, n);
   }
 
+  void propagateAsDecision(TNode n)
+    throw(AssertionException) {
+    push(PROPAGATE_AS_DECISION, n);
+  }
+
   LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 60e090d168df336a6bbd3bd3cbfafb0b288a94ba..76385219d3afaf53658fd3fe83472903ac8e7b74 100644 (file)
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -62,6 +62,11 @@ public:
     push(PROPAGATE, n);
   }
 
+  void propagateAsDecision(TNode n)
+    throw(AssertionException) {
+    // ignore
+  }
+
   LemmaStatus lemma(TNode n, bool removable)
     throw(AssertionException) {
     push(LEMMA, n);

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 2363e49061f30115094b47834357429ca75bd798..8d7bc9c72d68709069a1b6f5ed47b24133030061 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -54,6 +54,9 @@ class FakeOutputChannel : public OutputChannel {
   void propagate(TNode n) throw(AssertionException) {
     Unimplemented();
   }
+  void propagateAsDecision(TNode n) throw(AssertionException) {
+    Unimplemented();
+  }
   LemmaStatus lemma(TNode n, bool removable) throw(AssertionException) {
     Unimplemented();
   }