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)

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 73176ff8b3b5a61bfd72de7612e3b078980968d9..3a5b61390167b10e40e1f3d5ce8eb31093645677 100644 (file)
--- 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 8900b0e38efd8edcd27a270b4e69339d843ca213..f40031514ffe4160385c558c6cd9e4f2d9eb8223 100644 (file)
--- 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 17eaf80aaa68b3f4e2cc56e06037e69350e11446..b45874bf2bb6e476842a1340883e09613f95366d 100644 (file)
--- 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 1f43ede423b5f3a4818a7ea4721062e81ef525ac..58000e4351d8d53c895da0d6da9b05c59ee9e522 100644 (file)
--- 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 c8277be71499a20456246b4fe2951b554e1c6aec..9dd25740115f526ebe68c76ddf193f666eac957e 100644 (file)
--- 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)