Fix models involving cardinality of sets of finite type (#8206)

Was caused by a flag not being reset, thus making it so that subsequent models did not use exclusion sets.

Fixes #5402. (Fixes the last benchmark on that issue, the first two are fixed by #8201).

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 5abbaab5cdfd1edeb033d6b2f1ad1898e37a17cc..941a1305aaad4b84f39fd38d21699c9e8a94db7e 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -55,6 +55,7 @@ void CardinalityExtension::reset()
   d_eqc_to_card_term.clear();
   d_t_card_enabled.clear();
   d_finite_type_elements.clear();
+  d_finite_type_constants_processed = false;
   d_finite_type_slack_elements.clear();
   d_univProxy.clear();
 }
@@ -1101,21 +1102,26 @@ void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
   {
     return;
   }
+  Trace("sets-model-finite") << "Collect finite elements" << std::endl;
   for (const Node& set : getOrderedSetsEqClasses())
   {
+    Trace("sets-model-finite") << "eqc: " << set << std::endl;
     if (!d_env.isFiniteType(set.getType()))
     {
+      Trace("sets-model-finite") << "...not finite" << std::endl;
       continue;
     }
     if (!isModelValueBasic(set))
     {
       // only consider leaves in the cardinality graph
+      Trace("sets-model-finite") << "...not basic value" << std::endl;
       continue;
     }
     for (const std::pair<const Node, Node>& pair : d_state.getMembers(set))
     {
       Node member = pair.first;
       Node modelRepresentative = model->getRepresentative(member);
+      Trace("sets-model-finite") << "  member: " << member << std::endl;
       std::vector<Node>& elements = d_finite_type_elements[member.getType()];
       if (std::find(elements.begin(), elements.end(), modelRepresentative)
           == elements.end())
@@ -1125,6 +1131,7 @@ void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
     }
   }
   d_finite_type_constants_processed = true;
+  Trace("sets-model-finite") << "End Collect finite elements" << std::endl;
 }
 
 const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 129fbb85b10f8d315f080f4deb40bf6de5e8caec..9ebff31ceccffe16d6c72cf28f830435b93c41a1 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1217,6 +1217,7 @@ set(regress_0_tests
   regress0/sets/issue5400-card-minus-univ.smt2
   regress0/sets/issue5400-2-card-minus-univ.smt2
   regress0/sets/issue5402-1-card.smt2
+  regress0/sets/issue5402-2-card-finite.smt2 
   regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
   regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
   regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2

diff --git a/test/regress/regress0/sets/issue5402-2-card-finite.smt2 b/test/regress/regress0/sets/issue5402-2-card-finite.smt2
new file mode 100644 (file)
index 0000000..8b85867
--- /dev/null
+++ b/test/regress/regress0/sets/issue5402-2-card-finite.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(set-option :sets-ext true)
+(declare-datatype Color ((Blue) (Purple)))
+(declare-fun A () (Set Color))
+(assert (> (set.card A) 1))
+(check-sat)
+(check-sat)