From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 3 Dec 2014 16:38:36 +0000 (-0500)
Subject: Revert "Disable constants sharing in eq engine, disable hack in theory engine."
X-Git-Tag: cvc5-1.0.0~6479
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=160134dc043c28308865d2b91648ba412d0749d4;p=cvc5.git

Revert "Disable constants sharing in eq engine, disable hack in theory engine."

This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba.

In particular, it DOES NOT revert
  "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine."
which is part of the same commit.
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index eae76099e..9d91c096a 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1201,6 +1201,7 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
 }
 
 Node TheoryEngine::getModelValue(TNode var) {
+  if(var.isConst()) return var;  // FIXME: HACK!!!
   Assert(d_sharedTerms.isShared(var));
   return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
 }
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index d1f1e9ed3..3b19270a4 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -308,6 +308,22 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
     // We set this here as this only applies to actual terms, not the
     // intermediate application terms
     d_isBoolean[result] = true;
+  } else if (d_isConstant[result]) {
+    // Non-Boolean constants are trigger terms for all tags
+    EqualityNodeId tId = getNodeId(t);
+    // Setup the new set 
+    Theory::Set newSetTags = 0;
+    EqualityNodeId newSetTriggers[THEORY_LAST];
+    unsigned newSetTriggersSize = THEORY_LAST;
+    for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
+      newSetTags = Theory::setInsert(currentTheory, newSetTags);
+      newSetTriggers[currentTheory] = tId;
+    }
+    // Add it to the list for backtracking
+    d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
+    d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+    // Mark the the new set as a trigger
+    d_nodeIndividualTrigger[tId] = newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
   }
 
   // If this is not an internal node, add it to the master