adding simple-minded handling of (dis-)equalities where constants are involved

2 files changed, 28 insertions, 1 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index ec0a8fce3..f9220c7f3 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -76,6 +76,7 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name)
 , d_equalityTriggersCount(context, 0)
 , d_individualTriggersSize(context, 0)
 , d_constantRepresentativesSize(context, 0)
+, d_constantsSize(context, 0)
 , d_stats(name)
 {
   init();
@@ -92,6 +93,7 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 , d_equalityTriggersCount(context, 0)
 , d_individualTriggersSize(context, 0)
 , d_constantRepresentativesSize(context, 0)
+, d_constantsSize(context, 0)
 , d_stats(name)
 {
   init();
@@ -171,6 +173,24 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
 
   Debug("equality") << "EqualityEngine::newNode(" << node << ") => " << newId << std::endl;
 
+  // If the node is a constant, assert all the dis-eqalities
+  if (node.isConst() && node.getKind() != kind::CONST_BOOLEAN) {
+
+    TypeNode nodeType = node.getType();
+    for (unsigned i = 0; i < d_constants.size(); ++ i) {
+      TNode constant = d_constants[i];
+      if (constant.getType().isComparableTo(nodeType)) {
+        Debug("equality::constants") << "adding const dis-equality " << node << " != " << constant << std::endl;
+        assertEquality(node.eqNode(constant), false, d_true);
+      }
+    }
+
+    d_constants.push_back(node);
+    d_constantsSize = d_constantsSize + 1;
+
+    propagate();
+  }
+
   return newId;
 }
 
@@ -341,7 +361,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   } while (currentId != class2Id);
 
-
   // Update class2 table lookup and information
   Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
   do {
@@ -553,6 +572,8 @@ void EqualityEngine::backtrack() {
     d_equalityGraph.resize(d_nodesCount);
     d_equalityNodes.resize(d_nodesCount);
   }
+
+  d_constants.resize(d_constantsSize);
 }
 
 void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index f9c10d1b6..047e9de49 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -584,6 +584,12 @@ private:
   /** The list of representatives that became constant. */ 
   std::vector<EqualityNodeId> d_constantRepresentatives;
 
+  /** List of all the constants. */
+  std::vector<TNode> d_constants;
+
+  /** Size of the constants list */
+  context::CDO<unsigned> d_constantsSize;
+
   /**
    * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
    */