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 ef4f5124686044e954c6bc02b3cb6f1e2c892418..93b19c76a960bd4bf391ba54995a2b99011cdcd3 100644 (file)
--- 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 8bb0e3f15158e19b794bb09922cb870f4a1058d9..22bc205cd1d169a820529672f19643a0a41b9cd4 100644 (file)
--- 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 e150199eedfae0e3be1e0d9da361eacf4465a651..603f2b069b44974f80034cf56654e500fb058730 100644 (file)
--- 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 a39b7b344f9d72c85a6a7798b91d0cf40350e7b6..3d926c8e7e20ac1939039ffa543965de21ca52f9 100644 (file)
--- 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 (file)
index 0000000..d370639
--- /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)