From 8c92533a49b715a70d7ef187ef470901fd0c11c8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 29 Mar 2022 11:46:14 -0500 Subject: [PATCH] Fix issue related to use of Boolean term variable for set/bag choose (#8423) Fixes cvc5/cvc5-projects#501. I am considering making this detail internal to SkolemManager to avoid similar issues in the future. However, there are some subtle performance implications in doing so, so this will be addressed later. --- src/theory/bags/theory_bags.cpp | 8 +++++++- src/theory/sets/cardinality_extension.cpp | 7 ++++++- src/theory/sets/theory_sets.cpp | 2 +- src/theory/sets/theory_sets_private.cpp | 17 +++++++++++++++-- test/regress/cli/CMakeLists.txt | 1 + .../proj-issue501-choose-bool-term-var.smt2 | 12 ++++++++++++ 6 files changed, 42 insertions(+), 5 deletions(-) create mode 100644 test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index b1e9b32b7..3dae04861 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -117,7 +117,13 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node, NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Node x = sm->mkPurifySkolem(node, "bagChoose"); + // the skolem will occur in a term context, thus we give it Boolean + // term variable kind immediately. + SkolemManager::SkolemFlags flags = node.getType().isBoolean() + ? SkolemManager::SKOLEM_BOOL_TERM_VAR + : SkolemManager::SKOLEM_DEFAULT; + Node x = sm->mkPurifySkolem( + node, "bagChoose", "a variable used to eliminate bag choose", flags); Node A = node[0]; TypeNode bagType = A.getType(); TypeNode ufType = nm->mkFunctionType(bagType, bagType.getBagElementType()); diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 8f23e9232..b01895a74 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -1030,7 +1030,12 @@ void CardinalityExtension::mkModelValueElementsFor( { TypeNode elementType = eqc.getType().getSetElementType(); bool elementTypeFinite = d_env.isFiniteType(elementType); - if (isModelValueBasic(eqc)) + bool isBasic = isModelValueBasic(eqc); + Trace("sets-model") << "mkModelValueElementsFor: " << eqc + << ", isBasic = " << isBasic + << ", isFinite = " << elementTypeFinite + << ", els = " << els << std::endl; + if (isBasic) { std::map::iterator it = d_eqc_to_card_term.find(eqc); if (it != d_eqc_to_card_term.end()) diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index e61881daa..6d5de2172 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -218,7 +218,7 @@ void TheorySets::processCarePairArgs(TNode a, TNode b) // equality or disequality between members affects the number of elements // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER. // Example: - // Suppose (= (member x S) member(y S)) is true and there are + // Suppose (set.member x S) = (set.member y S) = true and there are // no other members in S. We would get S = {x} if (= x y) is true. // Otherwise we would get S = {x, y}. if (a.getKind() != SET_MEMBER && d_state.areEqual(a, b)) diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 099843e3c..57835919e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -247,7 +247,14 @@ void TheorySetsPrivate::fullEffortCheck() Node n = (*eqc_i); if (n != eqc) { - Trace("sets-eqc") << n << " (" << n.isConst() << ") "; + if (TraceIsOn("sets-eqc")) + { + Trace("sets-eqc") << n; + if (n.isConst()) + { + Trace("sets-eqc") << " (const) "; + } + } } TypeNode tnn = n.getType(); if (isSet) @@ -1211,7 +1218,13 @@ TrustNode TheorySetsPrivate::expandChooseOperator( NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Node x = sm->mkPurifySkolem(node, "setChoose"); + // the skolem will occur in a term context, thus we give it Boolean + // term variable kind immediately. + SkolemManager::SkolemFlags flags = node.getType().isBoolean() + ? SkolemManager::SKOLEM_BOOL_TERM_VAR + : SkolemManager::SKOLEM_DEFAULT; + Node x = sm->mkPurifySkolem( + node, "setChoose", "a variable used to eliminate set choose", flags); Node A = node[0]; TypeNode setType = A.getType(); ensureFirstClassSetType(setType); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 8db3689eb..000cbc376 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1263,6 +1263,7 @@ set(regress_0_tests regress0/sets/proj-issue177.smt2 regress0/sets/proj-issue486-sets-split-eq.smt2 regress0/sets/proj-issue493-choose-det.smt2 + regress0/sets/proj-issue501-choose-bool-term-var.smt2 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 regress0/sets/setel-eq.smt2 regress0/sets/sets-deq-dd.smt2 diff --git a/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 b/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 new file mode 100644 index 000000000..0fcdbdd25 --- /dev/null +++ b/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: -q +; EXPECT: sat +(set-logic ALL) +(set-option :sets-ext true) +(set-option :fmf-bound true) +(declare-const x (Bag (Set Bool))) +(declare-const x1 (Set Bool)) +(declare-const x3 (Set Bool)) +(declare-const x6 (Set Bool)) +(assert (set.choose (ite (set.is_singleton x3) x6 x1))) +(assert (<= (set.card x6) (bag.count x6 x))) +(check-sat) -- 2.30.2