Better getEqualityStatus for arrays, smarter combination of theories

4 files changed, 52 insertions, 22 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index e73c059d4..6b91400e8 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -566,12 +566,11 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
     // The terms are implied to be equal
     return EQUALITY_TRUE;
   }
-  if (d_equalityEngine.areDisequal(a, b, false)) {
+  else if (d_equalityEngine.areDisequal(a, b, false)) {
     // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
-  //TODO: can we be more precise sometimes?
-  return EQUALITY_UNKNOWN;
+  return EQUALITY_UNKNOWN;//FALSE_IN_MODEL;
 }
 
 
@@ -665,18 +664,17 @@ void TheoryArrays::computeCareGraph()
             // Should have been propagated to us
             Assert(false);
             break;
-          case EQUALITY_FALSE_AND_PROPAGATED:
-            // Should have been propagated to us
-            Assert(false);
-            break;
-          case EQUALITY_FALSE:
           case EQUALITY_TRUE:
             // Missed propagation - need to add the pair so that theory engine can force propagation
             Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): missed propagation" << std::endl;
             break;
+          case EQUALITY_FALSE_AND_PROPAGATED:
+            // Should have been propagated to us
+            Assert(false);
+          case EQUALITY_FALSE:
           case EQUALITY_FALSE_IN_MODEL:
-            Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl;
-            break;
+            // Don't need to include this pair
+            continue;
           default:
             break;
         }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 01387637e..ffe4258cd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -405,7 +405,7 @@ void TheoryEngine::check(Theory::Effort effort) {
       propagate(effort);
 
       // We do combination if all has been processed and we are in fullcheck
-      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded) {
+      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
         // Do the combination
         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
         combineTheories();
@@ -453,7 +453,7 @@ void TheoryEngine::check(Theory::Effort effort) {
 
 void TheoryEngine::combineTheories() {
 
-  Trace("sharing") << "TheoryEngine::combineTheories()" << endl;
+  Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl;
 
   TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
 
@@ -471,25 +471,46 @@ void TheoryEngine::combineTheories() {
   // Call on each parametric theory to give us its care graph
   CVC4_FOR_EACH_THEORY;
 
-  Trace("sharing") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl;
+  Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl;
 
   // Now add splitters for the ones we are interested in
   CareGraph::const_iterator care_it = careGraph.begin();
   CareGraph::const_iterator care_it_end = careGraph.end();
+
   for (; care_it != care_it_end; ++ care_it) {
     const CarePair& carePair = *care_it;
 
-    Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl;
+    Debug("combineTheories") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << endl;
 
     Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst());
     Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst());
 
     // The equality in question (order for no repetition)
     Node equality = carePair.a.eqNode(carePair.b);
+    EqualityStatus es = getEqualityStatus(carePair.a, carePair.b);
+    Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
+      (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
+      es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
+      es == EQUALITY_TRUE ? "EQUALITY_TRUE" :
+      es == EQUALITY_FALSE ? "EQUALITY_FALSE" :
+      es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" :
+      es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" :
+      es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" :
+       "Unexpected case") << endl;
 
     // We need to split on it
-    Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << endl;
+    Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
     lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory);
+    if (false) {
+      if (es == EQUALITY_TRUE_IN_MODEL) {
+        Node e = ensureLiteral(equality);
+        d_propEngine->requirePhase(e, true);
+      }
+      else if (es == EQUALITY_FALSE_IN_MODEL) {
+        Node e = ensureLiteral(equality);
+        d_propEngine->requirePhase(e, false);
+      }
+    }
   }
 }
 
@@ -1182,6 +1203,18 @@ Node TheoryEngine::getModelValue(TNode var) {
   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
 }
 
+
+Node TheoryEngine::ensureLiteral(TNode n) {
+  Debug("ensureLiteral") << "rewriting: " << n << std::endl;
+  Node rewritten = Rewriter::rewrite(n);
+  Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
+  Node preprocessed = preprocess(rewritten);
+  Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
+  d_propEngine->ensureLiteral(preprocessed);
+  return preprocessed;
+}
+
+
 void TheoryEngine::printInstantiations( std::ostream& out ) {
   if( d_quantEngine ){
     d_quantEngine->printInstantiations( out );
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index eec4f1168..e589e8f87 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -759,6 +759,11 @@ public:
   Node getModelValue(TNode var);
 
   /**
+   * Takes a literal and returns an equivalent literal that is guaranteed to be a SAT literal
+   */
+  Node ensureLiteral(TNode n);
+
+  /**
    * Print all instantiations made by the quantifiers module.
    */
   void printInstantiations( std::ostream& out );
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 72d878782..b2d7f4b21 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -88,13 +88,7 @@ Node Valuation::getModelValue(TNode var) {
 }
 
 Node Valuation::ensureLiteral(TNode n) {
-  Debug("ensureLiteral") << "rewriting: " << n << std::endl;
-  Node rewritten = Rewriter::rewrite(n);
-  Debug("ensureLiteral") << "      got: " << rewritten << std::endl;
-  Node preprocessed = d_engine->preprocess(rewritten);
-  Debug("ensureLiteral") << "preproced: " << preprocessed << std::endl;
-  d_engine->getPropEngine()->ensureLiteral(preprocessed);
-  return preprocessed;
+  return d_engine->ensureLiteral(n);
 }
 
 bool Valuation::isDecision(Node lit) const {