From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 05:12:08 +0000 (-0600)
Subject: Make blockModelValues robust to non-closed enumerable types (#8055)
X-Git-Tag: cvc5-1.0.0~348
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7910026d54c24c7ef1b58c0b90069142302c314;p=cvc5.git

Make blockModelValues robust to non-closed enumerable types (#8055)

Fixes cvc5/cvc5-projects#420.

Also fixes the trivial case where there is nothing to block, in which case we should add false (via mkOr) not true.
---

diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index cee38d83a..d5f70315e 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -255,26 +255,48 @@ Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
     // otherwise, block all terms that were specified in get-value
     else
     {
+      std::map<TypeNode, std::vector<Node> > nonClosedEnum;
+      std::map<Node, Node> nonClosedValue;
       std::unordered_set<Node> terms;
-      for (Node n : nodesToBlock)
+      for (const Node& n : nodesToBlock)
       {
+        TypeNode tn = n.getType();
         Node v = m->getValue(n);
-        Node a = nm->mkNode(DISTINCT, n, v);
-        blockers.push_back(a);
+        if (tn.isClosedEnumerable())
+        {
+          // if its type is closed enumerable, then we can block its value
+          Node a = n.eqNode(v).notNode();
+          blockers.push_back(a);
+        }
+        else
+        {
+          nonClosedValue[n] = v;
+          // otherwise we will block (dis)equality with other variables of its
+          // type below
+          nonClosedEnum[tn].push_back(n);
+        }
+      }
+      for (const std::pair<const TypeNode, std::vector<Node> >& es :
+           nonClosedEnum)
+      {
+        size_t nenum = es.second.size();
+        for (size_t i = 0; i < nenum; i++)
+        {
+          const Node& vi = nonClosedValue[es.second[i]];
+          for (size_t j = (i + 1); j < nenum; j++)
+          {
+            const Node& vj = nonClosedValue[es.second[j]];
+            Node eq = es.second[i].eqNode(es.second[j]);
+            if (vi == vj)
+            {
+              eq = eq.notNode();
+            }
+            blockers.push_back(eq);
+          }
+        }
       }
     }
-    if (blockers.size() == 0)
-    {
-      blocker = nm->mkConst<bool>(true);
-    }
-    else if (blockers.size() == 1)
-    {
-      blocker = blockers[0];
-    }
-    else
-    {
-      blocker = nm->mkNode(OR, blockers);
-    }
+    blocker = nm->mkOr(blockers);
   }
   Trace("model-blocker") << "...model blocker is " << blocker << std::endl;
   return blocker;
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 7234dc796..ac6e4543e 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3003,6 +3003,30 @@ TEST_F(TestApiBlackSolver, proj_issue414)
   ASSERT_NO_THROW(slv.simplify(t54));
 }
 
+TEST_F(TestApiBlackSolver, proj_issue420)
+{
+  Solver slv;
+  slv.setOption("strings-exp", "true");
+  slv.setOption("produce-models", "true");
+  slv.setOption("produce-unsat-cores", "true");
+  Sort s2 = slv.getRealSort();
+  Sort s3 = slv.mkUninterpretedSort("_u0");
+  DatatypeDecl _dt1 = slv.mkDatatypeDecl("_dt1", {});
+  DatatypeConstructorDecl _cons16 = slv.mkDatatypeConstructorDecl("_cons16");
+  _cons16.addSelector("_sel13", s3);
+  _dt1.addConstructor(_cons16);
+  std::vector<Sort> _s4 = slv.mkDatatypeSorts({_dt1});
+  Sort s4 = _s4[0];
+  Sort s5 = slv.mkSequenceSort(s2);
+  Term t3 = slv.mkConst(s5, "_x18");
+  Term t7 = slv.mkConst(s4, "_x22");
+  Term t13 = slv.mkTerm(Kind::DT_SIZE, {t7});
+  Term t53 = slv.mkTerm(Kind::SEQ_NTH, {t3, t13});
+  ASSERT_NO_THROW(slv.checkSat());
+  ASSERT_NO_THROW(slv.blockModelValues({t53, t7}));
+  ASSERT_NO_THROW(slv.checkSat());
+}
+
 TEST_F(TestApiBlackSolver, proj_issue440)
 {
   Solver slv;