Fix cvc5-projects issue 358 (#7804)

This PR fixes issue cvc5/cvc5-projects#358 which is caused by unregistered terms in the equality engine of bags

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 0694c179b83103619a3a9d209f8fbcefa474eada..39598975b862d05606c67834182d4c3256d62fea 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -260,18 +260,7 @@ bool TheoryBags::collectModelValues(TheoryModel* m,
     {
       Node key = d_state.getRepresentative(e);
       Node countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, r);
-      context::CDList<TNode>::const_iterator shared_it =
-          std::find(d_sharedTerms.begin(), d_sharedTerms.end(), countTerm);
-      eq::EqClassIterator it =
-          eq::EqClassIterator(r, d_state.getEqualityEngine());
-      while (!it.isFinished() && shared_it == d_sharedTerms.end())
-      {
-        Node bag = *(++it);
-        countTerm = NodeManager::currentNM()->mkNode(BAG_COUNT, e, bag);
-        shared_it =
-            std::find(d_sharedTerms.begin(), d_sharedTerms.end(), countTerm);
-      }
-      Node value = d_valuation.getModelValue(countTerm);
+      Node value = m->getRepresentative(countTerm);
       elementReps[key] = value;
     }
     Node rep = NormalForm::constructBagFromElements(tn, elementReps);
@@ -289,9 +278,15 @@ Node TheoryBags::getModelValue(TNode node) { return Node::null(); }
 
 void TheoryBags::preRegisterTerm(TNode n)
 {
-  Trace("bags::TheoryBags::preRegisterTerm") << n << std::endl;
+  Trace("bags") << "TheoryBags::preRegisterTerm(" << n << ")" << std::endl;
   switch (n.getKind())
   {
+    case kind::EQUAL:
+    {
+      // add trigger predicate for equality and membership
+      d_equalityEngine->addTriggerPredicate(n);
+    }
+    break;
     case BAG_FROM_SET:
     case BAG_TO_SET:
     case BAG_IS_SINGLETON:
@@ -300,7 +295,7 @@ void TheoryBags::preRegisterTerm(TNode n)
       ss << "Term of kind " << n.getKind() << " is not supported yet";
       throw LogicException(ss.str());
     }
-    default: break;
+    default: d_equalityEngine->addTerm(n); break;
   }
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ffff25520dc4fbaa6948f414fcdad4f10548f765..6943b72508bbe17cf522cc36b25a779dac4066d2 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1631,6 +1631,7 @@ set(regress_1_tests
   regress1/bags/map-lazy-lam.smt2
   regress1/bags/murxla1.smt2
   regress1/bags/murxla2.smt2
+  regress1/bags/murxla3.smt2
   regress1/bags/subbag1.smt2
   regress1/bags/subbag2.smt2
   regress1/bags/union_disjoint.smt2

diff --git a/test/regress/regress1/bags/murxla3.smt2 b/test/regress/regress1/bags/murxla3.smt2
new file mode 100644 (file)
index 0000000..3bfce38
--- /dev/null
+++ b/test/regress/regress1/bags/murxla3.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const A (Bag Bool))
+(set-info :status sat)
+(declare-fun p ((Bag Bool)) Bool)
+(assert (or (not (p A)) (not (p (as bag.empty (Bag Bool))))))
+(check-sat)