Fix for registration issues of term appearing in a shared lemma

(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)

5 files changed, 27 insertions, 1 deletions

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 73176ff8b..3a5b61390 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -34,6 +34,10 @@ TheorySets::~TheorySets() {
   delete d_internal;
 }
 
+void TheorySets::addSharedTerm(TNode n) {
+  d_internal->addSharedTerm(n);
+}
+
 void TheorySets::check(Effort e) {
   d_internal->check(e);
 }
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 8900b0e38..f40031514 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -46,6 +46,8 @@ public:
 
   ~TheorySets();
 
+  void addSharedTerm(TNode);
+
   void check(Effort);
 
   void collectModelInfo(TheoryModel*, bool fullModel);
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 17eaf80aa..b45874bf2 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -54,6 +54,19 @@ void TheorySetsPrivate::check(Theory::Effort level) {
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
 
+    if (!assertion.isPreregistered) {
+      if (atom.getKind() == kind::EQUAL) {
+        if (!d_equalityEngine.hasTerm(atom[0])) {
+          Assert(atom[0].isConst());
+          d_equalityEngine.addTerm(atom[0]);
+        }
+        if (!d_equalityEngine.hasTerm(atom[1])) {
+          Assert(atom[1].isConst());
+          d_equalityEngine.addTerm(atom[1]);
+        }
+      }
+    }
+
     // Solve each
     switch(atom.getKind()) {
     case kind::EQUAL:
@@ -710,6 +723,11 @@ bool TheorySetsPrivate::propagate(TNode literal) {
 }/* TheorySetsPropagate::propagate(TNode) */
 
 
+void TheorySetsPrivate::addSharedTerm(TNode n) {
+  Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
+  d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
+}
+
 void TheorySetsPrivate::conflict(TNode a, TNode b)
 {
   if (a.getKind() == kind::CONST_BOOLEAN) {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 1f43ede42..58000e435 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -47,6 +47,8 @@ public:
 
   ~TheorySetsPrivate();
 
+  void addSharedTerm(TNode);
+
   void check(Theory::Effort);
 
   void collectModelInfo(TheoryModel*, bool fullModel);
diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2
index c8277be71..9dd257401 100644
--- a/test/regress/regress0/sets/sets-testlemma-ints.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2
@@ -3,5 +3,5 @@
 (set-info :status sat)
 (declare-fun x () (Set Int))
 (declare-fun y () (Set Int))
-(assert (= x y))
+(assert (not (= x y)))
 (check-sat)