Make model core robust to when we cannot show the model satisfies input (#8811)

Fixes #8807.

diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index f2d84594b7b2561ad721cd039fbe80274246a2dd..8d784c2fcffc67c5d92f93f1be7828ebf492673f 100644 (file)
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -79,36 +79,27 @@ bool ModelCoreBuilder::setModelCore(const std::vector<Node>& assertions,
   Trace("model-core") << "Minimizing substitution..." << std::endl;
   std::vector<Node> coreVars;
   std::vector<Node> impliedVars;
-  bool minimized = false;
   theory::SubstitutionMinimize sm(d_env);
   if (mode == options::ModelCoresMode::NON_IMPLIED)
   {
-    minimized = sm.findWithImplied(formula, vars, subs, coreVars, impliedVars);
+    sm.findWithImplied(formula, vars, subs, coreVars, impliedVars);
   }
   else if (mode == options::ModelCoresMode::SIMPLE)
   {
-    minimized = sm.find(formula, truen, vars, subs, coreVars);
+    sm.find(formula, truen, vars, subs, coreVars);
   }
   else
   {
     Unreachable() << "Unknown model cores mode";
   }
-  Assert(minimized)
-      << "cannot compute model core, since model does not satisfy input!";
-  if (minimized)
-  {
-    m->setUsingModelCore();
-    Trace("model-core") << "...got core vars : " << coreVars << std::endl;
+  m->setUsingModelCore();
+  Trace("model-core") << "...got core vars : " << coreVars << std::endl;
 
-    for (const Node& cv : coreVars)
-    {
-      m->recordModelCoreSymbol(cv);
-    }
-    return true;
+  for (const Node& cv : coreVars)
+  {
+    m->recordModelCoreSymbol(cv);
   }
-  Trace("model-core") << "...failed, model does not satisfy input!"
-                      << std::endl;
-  return false;
+  return true;
 }
 
 }  // namespace cvc5::internal

diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp
index 96e5c9b171bb2e45461addc3699682a1323317d9..e0a107bf463979146aa7e8d909284613e52d0928 100644 (file)
--- a/src/theory/subs_minimize.cpp
+++ b/src/theory/subs_minimize.cpp
@@ -258,6 +258,14 @@ bool SubstitutionMinimize::findInternal(Node n,
   if (value[n] != target)
   {
     Trace("subs-min") << "... not equal to target " << target << std::endl;
+    // depends on all variables
+    for (const std::pair<const TNode, Node>& v : value)
+    {
+      if (v.first.isVar())
+      {
+        reqVars.push_back(v.first);
+      }
+    }
     return false;
   }
 

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 24d311604173f25af100b3e01c012dc98825d855..5156d97df3845c093e3385a82175cc2b267c0ba0 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -753,6 +753,7 @@ set(regress_0_tests
   regress0/issue6605-2-abd-triv.smt2
   regress0/issue6738.smt2
   regress0/issue6741.smt2
+  regress0/issue8807-model-core-partial.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
   regress0/ite_real_valid.smtv1.smt2

diff --git a/test/regress/cli/regress0/issue8807-model-core-partial.smt2 b/test/regress/cli/regress0/issue8807-model-core-partial.smt2
new file mode 100644 (file)
index 0000000..4daaf2c
--- /dev/null
+++ b/test/regress/cli/regress0/issue8807-model-core-partial.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --model-cores=simple -q
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () (Bag String)) 
+(assert (= (bag.choose a) "")) 
+(check-sat)