From: mudathirmahgoub 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> set = - std::make_shared>(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> set = + std::make_shared>(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)