Revert "Disable constants sharing in eq engine, disable hack in theory engine."
authorKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 3 Dec 2014 16:38:36 +0000 (11:38 -0500)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 3 Dec 2014 16:39:07 +0000 (11:39 -0500)
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.

src/theory/theory_engine.cpp
src/theory/uf/equality_engine.cpp

index eae76099e5b184effe22b5d632ba202d27657dea..9d91c096a6c19b48f3cf097882bda02225fe7cc2 100644 (file)
@@ -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);
 }
index d1f1e9ed3cfc5ea8c71043dd10cb851b3a4b3852..3b19270a48f3054fb0391997d18e1e72896b4383 100644 (file)
@@ -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