From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 22:36:05 +0000 (-0600)
Subject: Fix models involving cardinality of sets of finite type (#8206)
X-Git-Tag: cvc5-1.0.0~339
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c1569c97f1d2a08c528ebddb86454bfa6ea58611;p=cvc5.git

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 5abbaab5c..941a1305a 100644
--- 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 129fbb85b..9ebff31ce 100644
--- 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
index 000000000..8b8586700
--- /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)