Separate ill-typed portion of arith models (#8734)

This makes it so that the ill-typed portion of arithmetic models is not included in the main arithModel map.

Conceptually, we should not include entries in the arithmetic model that violate type constraints since these should never be used e.g. in non-linear to justify whether a model is correct. Instead, by not including that value, we assume that no value was given for that variable. Sanity checking of the arithmetic model then needs only to access the ill-typed portion of the model directly.

This makes it so that strict type invariants can be enforced in the non-linear solver's model.

diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp
index 67cc9d702baa8ff1bfe5e33a2a89ef798a01ad7c..aafeb43cbc719ff6482568cf17ec03fe0933fe8e 100644 (file)
--- a/src/theory/arith/linear/theory_arith_private.cpp
+++ b/src/theory/arith/linear/theory_arith_private.cpp
@@ -989,7 +989,6 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(
         // substitution is integral
         Trace("simplify") << "TheoryArithPrivate::solve(): substitution "
                           << minVar << " |-> " << elim << endl;
-
         outSubstitutions.addSubstitutionSolved(minVar, elim, tin);
         return Theory::PP_ASSERT_STATUS_SOLVED;
       }
@@ -3857,8 +3856,10 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{
   return belowMin;
 }
 
-void TheoryArithPrivate::collectModelValues(const std::set<Node>& termSet,
-                                            std::map<Node, Node>& arithModel)
+void TheoryArithPrivate::collectModelValues(
+    const std::set<Node>& termSet,
+    std::map<Node, Node>& arithModel,
+    std::map<Node, Node>& arithModelIllTyped)
 {
   AlwaysAssert(d_qflraStatus == Result::SAT);
 
@@ -3895,13 +3896,22 @@ void TheoryArithPrivate::collectModelValues(const std::set<Node>& termSet,
           // integer variables in rare cases. We construct real in this case;
           // this will be corrected in TheoryArith::sanityCheckIntegerModel.
           qNode = nm->mkConstReal(qmodel);
+          if (term.getType().isInteger())
+          {
+            Trace("arith::collectModelInfo")
+                << "add to arithModelIllTyped " << term << " -> " << qNode
+                << std::endl;
+            // in this case, we add to the ill-typed map instead of the main map
+            arithModelIllTyped[term] = qNode;
+            continue;
+          }
         }
         else
         {
           qNode = nm->mkConstRealOrInt(term.getType(), qmodel);
         }
-        Trace("arith::collectModelInfo") << "m->assertEquality(" << term << ", "
-                                         << qNode << ", true)" << endl;
+        Trace("arith::collectModelInfo")
+            << "add to arithModel " << term << " -> " << qNode << std::endl;
         // Add to the map
         arithModel[term] = qNode;
       }else{

diff --git a/src/theory/arith/linear/theory_arith_private.h b/src/theory/arith/linear/theory_arith_private.h
index 253f4b3a5060efa4c51fa44ccc5b5799c105fcc4..fdc67fc0c3d2eeec4af69679135042a576e17d7e 100644 (file)
--- a/src/theory/arith/linear/theory_arith_private.h
+++ b/src/theory/arith/linear/theory_arith_private.h
@@ -454,11 +454,16 @@ private:
    * non-linear extension) can modify arithModel before it is sent to the model.
    *
    * @param termSet The set of relevant terms
-   * @param arithModel Mapping from terms (of real type) to their values. The
-   * caller should assert equalities to the model for each entry in this map.
+   * @param arithModel Mapping from terms (of int/real type) to their values.
+   * The caller should assert equalities to the model for each entry in this
+   * map.
+   * @param arithModelIllTyped Mapping from terms (of int type) to real values.
+   * This is used for catching cases where this solver mistakenly set an
+   * integer variable to a real.
    */
   void collectModelValues(const std::set<Node>& termSet,
-                          std::map<Node, Node>& arithModel);
+                          std::map<Node, Node>& arithModel,
+                          std::map<Node, Node>& arithModelIllTyped);
 
   void shutdown(){ }
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b9b57599838e1d5559f0f18cd04343d90265fa46..4e8e1a40928ab75f432348d52c7cc3bad146ca0b 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -197,6 +197,7 @@ void TheoryArith::postCheck(Effort level)
   if (Theory::fullEffort(level))
   {
     d_arithModelCache.clear();
+    d_arithModelCacheIllTyped.clear();
     d_arithModelCacheSet = false;
     std::set<Node> termSet;
     if (d_nonlinearExtension != nullptr)
@@ -372,7 +373,8 @@ void TheoryArith::updateModelCache(std::set<Node>& termSet)
   {
     d_arithModelCacheSet = true;
     collectAssertedTerms(termSet);
-    d_internal->collectModelValues(termSet, d_arithModelCache);
+    d_internal->collectModelValues(
+        termSet, d_arithModelCache, d_arithModelCacheIllTyped);
   }
 }
 void TheoryArith::updateModelCache(const std::set<Node>& termSet)
@@ -380,48 +382,54 @@ void TheoryArith::updateModelCache(const std::set<Node>& termSet)
   if (!d_arithModelCacheSet)
   {
     d_arithModelCacheSet = true;
-    d_internal->collectModelValues(termSet, d_arithModelCache);
+    d_internal->collectModelValues(
+        termSet, d_arithModelCache, d_arithModelCacheIllTyped);
   }
 }
 bool TheoryArith::sanityCheckIntegerModel()
 {
-
-    // Double check that the model from the linear solver respects integer types,
-    // if it does not, add a branch and bound lemma. This typically should never
-    // be necessary, but is needed in rare cases.
-    bool addedLemma = false;
-    bool badAssignment = false;
-    Trace("arith-check") << "model:" << std::endl;
-    for (const auto& p : d_arithModelCache)
+  // Double check that the model from the linear solver respects integer types,
+  // if it does not, add a branch and bound lemma. This typically should never
+  // be necessary, but is needed in rare cases.
+  if (Configuration::isAssertionBuild())
+  {
+    for (CVC5_UNUSED const auto& p : d_arithModelCache)
     {
-      Trace("arith-check") << p.first << " -> " << p.second << std::endl;
-      if (p.first.getType().isInteger() && !p.second.getType().isInteger())
-      {
-        warning() << "TheoryArithPrivate generated a bad model value for "
-                     "integer variable "
-                  << p.first << " : " << p.second << std::endl;
-        // must branch and bound
-        TrustNode lem =
-            d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());
-        if (d_im.trustedLemma(lem, InferenceId::ARITH_BB_LEMMA))
-        {
-          addedLemma = true;
-        }
-        badAssignment = true;
-      }
+      // will change to strict type equal
+      Assert(p.second.getType().isSubtypeOf(p.second.getType()));
     }
-    if (addedLemma)
+  }
+  bool addedLemma = false;
+  bool badAssignment = false;
+  Trace("arith-check") << "model:" << std::endl;
+  for (const auto& p : d_arithModelCacheIllTyped)
+  {
+    Trace("arith-check") << p.first << " -> " << p.second << std::endl;
+    Assert(p.first.getType().isInteger() && !p.second.getType().isInteger());
+    warning() << "TheoryArithPrivate generated a bad model value for "
+                 "integer variable "
+              << p.first << " : " << p.second << std::endl;
+    // must branch and bound
+    TrustNode lem =
+        d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());
+    if (d_im.trustedLemma(lem, InferenceId::ARITH_BB_LEMMA))
     {
-      // we had to add a branch and bound lemma since the linear solver assigned
-      // a non-integer value to an integer variable.
-      return true;
+      addedLemma = true;
     }
-    // this would imply that linear arithmetic's model failed to satisfy a branch
-    // and bound lemma
-    AlwaysAssert(!badAssignment)
-        << "Bad assignment from TheoryArithPrivate::collectModelValues, and no "
-          "branching lemma was sent";
-    return false;
+    badAssignment = true;
+  }
+  if (addedLemma)
+  {
+    // we had to add a branch and bound lemma since the linear solver assigned
+    // a non-integer value to an integer variable.
+    return true;
+  }
+  // this would imply that linear arithmetic's model failed to satisfy a branch
+  // and bound lemma
+  AlwaysAssert(!badAssignment)
+      << "Bad assignment from TheoryArithPrivate::collectModelValues, and no "
+         "branching lemma was sent";
+  return false;
 }
 
 }  // namespace arith

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index c6ced57815dc7c62e490cbbdb4793086666aca67..62a15c7a820b8ba00d05036a4a7c2fde4264feb0 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -183,6 +183,8 @@ class TheoryArith : public Theory {
    * used to augment the TheoryModel.
    */
   std::map<Node, Node> d_arithModelCache;
+  /** Component of the above that was ill-typed */
+  std::map<Node, Node> d_arithModelCacheIllTyped;
   /** Is the above map computed? */
   bool d_arithModelCacheSet;