From: Andrew Reynolds Date: Fri, 6 May 2022 21:40:49 +0000 (-0500) Subject: Separate ill-typed portion of arith models (#8734) X-Git-Tag: cvc5-1.0.1~161 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0c9e8f57125695d0c16e1bff565113879a445baa;p=cvc5.git 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 67cc9d702..aafeb43cb 100644 --- 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& termSet, - std::map& arithModel) +void TheoryArithPrivate::collectModelValues( + const std::set& termSet, + std::map& arithModel, + std::map& arithModelIllTyped) { AlwaysAssert(d_qflraStatus == Result::SAT); @@ -3895,13 +3896,22 @@ void TheoryArithPrivate::collectModelValues(const std::set& 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 253f4b3a5..fdc67fc0c 100644 --- 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& termSet, - std::map& arithModel); + std::map& arithModel, + std::map& arithModelIllTyped); void shutdown(){ } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b9b575998..4e8e1a409 100644 --- 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 termSet; if (d_nonlinearExtension != nullptr) @@ -372,7 +373,8 @@ void TheoryArith::updateModelCache(std::set& 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& termSet) @@ -380,48 +382,54 @@ void TheoryArith::updateModelCache(const std::set& 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()); - 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()); + 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 c6ced5781..62a15c7a8 100644 --- 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 d_arithModelCache; + /** Component of the above that was ill-typed */ + std::map d_arithModelCacheIllTyped; /** Is the above map computed? */ bool d_arithModelCacheSet;