Fixed warning in decision_engine.h, minor tweak to caregraph function in

arrays, fixed bug with equalities between constants in shared terms database

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 1e6e8a64dbe6b20f0118a9f15d12f5023d26a50e..3ec6aaf2aae94bdecde9e11bc1ae4c5b1007a2d2 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -46,9 +46,9 @@ class DecisionEngine {
   CnfStream* d_cnfStream;
   DPLLSatSolverInterface* d_satSolver;
 
+  context::Context* d_satContext;
   SatValue d_result;
 
-  context::Context* d_satContext;
 public:
   // Necessary functions
 

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index c02f90bf08085abeece284cb71e27bdcd54f70b9..a62ebed06330968ea0af3ed24c2f0ac5677a3441 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -637,19 +637,21 @@ void TheoryArrays::computeCareGraph()
 
         EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
         switch (eqStatusDomain) {
-          case EQUALITY_FALSE_AND_PROPAGATED:
-          case EQUALITY_FALSE:
-            continue;
-            break;
           case EQUALITY_TRUE_AND_PROPAGATED:
-          case EQUALITY_TRUE:
             // Should have been propagated to us
             Assert(false);
+            break;
+          case EQUALITY_FALSE_AND_PROPAGATED:
+            // TODO: eventually this should be an Assert(false), but for now, disequalities are not propagated
             continue;
             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_IN_MODEL:
-            Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model, skipping" << std::endl;
-            continue;
+            Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl;
             break;
           default:
             break;

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 24cbc165c7cbffb45d0c21173f42764e9d3eeca4..577e1b957f202574d38b9aeb7b02234cf8632b96 100644 (file)
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -204,11 +204,9 @@ void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b)
     // Normalize the equality
     Node equality = left.eqNode(right);
     Node normalized = Rewriter::rewriteEquality(currentTheory, equality);
-    if (normalized.getKind() != kind::CONST_BOOLEAN) {
+    if (normalized.getKind() != kind::CONST_BOOLEAN || !normalized.getConst<bool>()) {
       // Notify client
       d_sharedNotify.notify(normalized, equality, currentTheory);
-    } else {
-      Assert(equality.getConst<bool>());
     }
   }
 
@@ -253,6 +251,7 @@ void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason)
   if (negated) {
     Assert(!d_equalityEngine.areDisequal(atom[0], atom[1]));
     d_equalityEngine.addDisequality(atom[0], atom[1], reason);
+    //    !!! need to send this out
   }
   else {
     Assert(!d_equalityEngine.areEqual(atom[0], atom[1]));

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1bb830aa847a063f2df3342659c482a6b1028a86..46a9f58554e936fcc2cf5bbec3ddb8d71cebddb1 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -936,3 +936,20 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     lemma(conflict, true, false);
   }
 }
+
+
+//Conflict from shared terms database
+void TheoryEngine::sharedConflict(TNode conflict) {
+  // Mark that we are in conflict
+  d_inConflict = true;
+
+  if(Dump.isOn("t-conflicts")) {
+    Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
+                        << CheckSatCommand(conflict.toExpr());
+  }
+
+  Node fullConflict = explain(ExplainTask(d_sharedTerms.explain(conflict), SHARED_DATABASE_EXPLANATION));
+  Assert(properConflict(fullConflict));
+  Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl;
+  lemma(fullConflict, true, false);
+}

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index dd642a865e8e055f327c9658946c82a5c226a7f1..faa6bbd269c0a49dea5903734991a0f95307c461 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -278,6 +278,11 @@ class TheoryEngine {
    */
   void conflict(TNode conflict, theory::TheoryId theoryId);
 
+  /**
+   * Called by shared terms database to notify of a conflict.
+   */
+  void sharedConflict(TNode conflict);
+
   /**
    * Debugging flag to ensure that shutdown() is called before the
    * destructor.
@@ -353,7 +358,13 @@ class TheoryEngine {
 
   void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory)
   {
-    d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
+    if (literal.getKind() == kind::CONST_BOOLEAN) {
+      Assert(!literal.getConst<bool>());
+      sharedConflict(original);
+    }
+    else {
+      d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
+    }
   }
 
   /**