Fix issue 5309 (#5327)

This PR fixes #5309 by ensuring singleton terms are added to the model builder as representatives.

Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index db2f3f22f05160ab925dc0edd16f831e657fa5e1..b951d03339f5fb4c5747f4a4f3bd452c22299760 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1112,6 +1112,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
         // cardinality
         d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals, m);
       }
+
       Node rep = NormalForm::mkBop(kind::UNION, els, eqc.getType());
       rep = Rewriter::rewrite(rep);
       Trace("sets-model") << "* Assign representative of " << eqc << " to "
@@ -1123,6 +1124,21 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
       }
       m->assertSkeleton(rep);
 
+      // we add the element terms (singletons) as representatives to tell the
+      // model builder to evaluate them along with their union (rep).
+      // This is needed to account for cases when members and rep are not enough
+      // for the model builder to evaluate set terms.
+      // e.g.
+      // eqc(rep) = [(union (singleton skolem) (singleton 0))]
+      // eqc(skolem) = [0]
+      // The model builder would fail to evaluate rep as (singleton 0)
+      // if (singleton skolem) is not registered as a representative in the
+      // model
+      for (const Node& el : els)
+      {
+        m->assertSkeleton(el);
+      }
+
       Trace("sets-model") << "Set " << eqc << " = { " << traceElements(rep)
                           << " }" << std::endl;
     }

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 2f9e168c90bb3137ad767a1ba830fe792eb64138..1fc609632abf2f165f4b24380ea37a7a673ca092 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -1185,13 +1185,19 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
           if (itMap != d_constantReps.end())
           {
             ri = (*itMap).second;
+            Trace("model-builder-debug") << i << ": const child " << ri << std::endl;
             recurse = false;
           }
           else if (!evalOnly)
           {
             recurse = false;
+            Trace("model-builder-debug") << i << ": keep " << ri << std::endl;
           }
         }
+        else
+        {
+          Trace("model-builder-debug") << i << ": no hasTerm " << ri << std::endl;
+        }
         if (recurse)
         {
           ri = normalize(m, ri, evalOnly);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 583b129c736f35d0ef598eae02a1cf7438ad85ec..6c2c51dfb9cf9443e8cb87763a11beccbbad3a42 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1790,6 +1790,7 @@ set(regress_1_tests
   regress1/sets/issue2568.smt2
   regress1/sets/issue2904.smt2
   regress1/sets/issue4391-card-lasso.smt2
+  regress1/sets/issue5309.smt2
   regress1/sets/lemmabug-ListElts317minimized.smt2
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2

diff --git a/test/regress/regress1/sets/issue5309.smt2 b/test/regress/regress1/sets/issue5309.smt2
new file mode 100644 (file)
index 0000000..383b126
--- /dev/null
+++ b/test/regress/regress1/sets/issue5309.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const zero Int)
+(declare-fun A () (Set Int))
+(assert (exists ((x Int)) (= A (singleton x))))
+(assert (member (- zero) A))
+(check-sat)