From e09c7d12441e55fe942ae573b49b880431cf1af1 Mon Sep 17 00:00:00 2001
From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Thu, 22 Oct 2020 11:48:25 -0500
Subject: [PATCH] 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
---
 src/theory/sets/theory_sets_private.cpp   | 16 ++++++++++++++++
 src/theory/theory_model_builder.cpp       |  6 ++++++
 test/regress/CMakeLists.txt               |  1 +
 test/regress/regress1/sets/issue5309.smt2 |  7 +++++++
 4 files changed, 30 insertions(+)
 create mode 100644 test/regress/regress1/sets/issue5309.smt2

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index db2f3f22f..b951d0333 100644
--- 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 2f9e168c9..1fc609632 100644
--- 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 583b129c7..6c2c51dfb 100644
--- 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
index 000000000..383b1263e
--- /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)
-- 
2.30.2