diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-19 15:35:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-19 20:35:13 +0000 |
commit | 8fe459b1fb3843ebdbda86f24a414c46b986aa90 (patch) | |
tree | 88b5233b226f8079b568ec8f4eaedaf67306f5c9 /src/theory/arith | |
parent | 71842aa75ca106b14ded148a73ac856f3ecf5912 (diff) |
Fix issue related to sanity checking integer models (#7363)
We now insist that we sanity check integer models in linear logics. Previously, we could trigger an assertion failure in Minisat if a user asked for a model in a state where the linear solver had assigned a real value to an integer variable, as we would be sending a lemma during collectModelValues in a state where we had already terminated with "sat".
This also changes an assertion to warning, to allow the regression to pass.
Fixes #6774 (This PR fixes a followup issue after the original bad model reported there was fixed by sanity checks).
As the assertion failure is downgraded to a warning, fixes #6988, fixes #7252.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 76a0c363d..cf2373b9f 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -193,9 +193,9 @@ void TheoryArith::postCheck(Effort level) if (Theory::fullEffort(level)) { d_arithModelCache.clear(); + std::set<Node> termSet; if (d_nonlinearExtension != nullptr) { - std::set<Node> termSet; updateModelCache(termSet); d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet); } @@ -204,6 +204,15 @@ void TheoryArith::postCheck(Effort level) // set incomplete d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED); } + // If we won't be doing a last call effort check (which implies that + // models will be computed), we must sanity check the integer model + // from the linear solver now. We also must update the model cache + // if we did not do so above. + if (d_nonlinearExtension == nullptr) + { + updateModelCache(termSet); + } + sanityCheckIntegerModel(); } } @@ -274,12 +283,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m, updateModelCache(termSet); - if (sanityCheckIntegerModel()) - { - // We added a lemma - return false; - } - // We are now ready to assert the model. for (const std::pair<const Node, Node>& p : d_arithModelCache) { @@ -383,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel() Trace("arith-check") << p.first << " -> " << p.second << std::endl; if (p.first.getType().isInteger() && !p.second.getType().isInteger()) { - Assert(false) << "TheoryArithPrivate generated a bad model value for " - "integer variable " - << p.first << " : " << p.second; + Warning() << "TheoryArithPrivate generated a bad model value for " + "integer variable " + << p.first << " : " << p.second; // must branch and bound TrustNode lem = d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>()); |