From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Mon, 18 Jul 2022 13:46:39 +0000 (-0500)
Subject: Fix issue 8959 (#8962)
X-Git-Tag: cvc5-1.0.1~4
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f069c8ea7b4c57290c2e9462b9e388d7ba4cb798;p=cvc5.git

Fix issue 8959 (#8962)

This PR fixes issue #8959 which happens because group terms that are not representatives are not registered in the solver state.
---

diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
index ef4f51246..93b19c76a 100644
--- a/src/theory/bags/solver_state.cpp
+++ b/src/theory/bags/solver_state.cpp
@@ -39,12 +39,6 @@ void SolverState::registerBag(TNode n)
 {
   Assert(n.getType().isBag());
   d_bags.insert(n);
-  if (n.getKind() == TABLE_GROUP)
-  {
-    std::shared_ptr<context::CDHashSet<Node>> set =
-        std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
-    d_partElementSkolems[n] = set;
-  }
 }
 
 void SolverState::registerCountTerm(Node bag, Node element, Node skolem)
@@ -61,6 +55,13 @@ void SolverState::registerCountTerm(Node bag, Node element, Node skolem)
   }
 }
 
+void SolverState::registerGroupTerm(Node n)
+{
+  std::shared_ptr<context::CDHashSet<Node>> set =
+      std::make_shared<context::CDHashSet<Node>>(d_env.getUserContext());
+  d_partElementSkolems[n] = set;
+}
+
 void SolverState::registerCardinalityTerm(Node n, Node skolem)
 {
   Assert(n.getKind() == BAG_CARD);
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index 8bb0e3f15..22bc205cd 100644
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -50,6 +50,9 @@ class SolverState : public TheoryState
    */
   void registerCountTerm(Node bag, Node element, Node skolem);
 
+  /** register a table.group term */
+  void registerGroupTerm(Node n);
+
   /**
    * store cardinality term and its skolem in a cahce
    * @param n has the form (bag.card A) where A is a representative
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index e150199ee..603f2b069 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -206,6 +206,10 @@ void TheoryBags::collectBagsAndCountTerms()
       {
         d_ig.registerCardinalityTerm(n);
       }
+      if (k == TABLE_GROUP)
+      {
+        d_state.registerGroupTerm(n);
+      }
       ++it;
     }
     Trace("bags-eqc") << " } " << std::endl;
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index a39b7b344..3d926c8e7 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1828,6 +1828,7 @@ set(regress_1_tests
   regress1/bags/intersection_min1.smt2
   regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2
+  regress1/bags/issue_8959.smt2
   regress1/bags/map1.smt2
   regress1/bags/map2.smt2
   regress1/bags/map3.smt2
diff --git a/test/regress/cli/regress1/bags/issue_8959.smt2 b/test/regress/cli/regress1/bags/issue_8959.smt2
new file mode 100644
index 000000000..d370639e1
--- /dev/null
+++ b/test/regress/cli/regress1/bags/issue_8959.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun e () (Table String String String))
+(assert (= (table.group e) (bag (bag (tuple "" "" "") 1) 1)))
+(check-sat)