1 files changed, 62 insertions, 17 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 6385d1467..be1c3abaf 100644
--- 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;
 
@@ -331,6 +344,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
    */
   void propagate(TNode literal, theory::TheoryId theory);
@@ -342,6 +368,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.
    */
   bool d_lemmasAdded;
@@ -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 */