diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-29 10:28:27 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-29 10:28:27 -0600 |
commit | ee75ebf00e1aa463656cd192e52d3aec224345c0 (patch) | |
tree | 5b34e2133c6d19f2264e4994379f5dc81209239e /src | |
parent | 31efb570a9d5811fd88a34d4915d7d08c81d13fa (diff) |
Throw warning instead of error for non-constant values in check-model stages (#3844)
Fixes #3729 and fixes #3720.
This updates two more stages of check-model (checking whether values assigned to terms are constants and internally checking whether assertions belonging to theories) to only throw warnings when a term/assertion has a non-constant value in the model. This is to accommodate cases where check-model is infeasible.
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 23 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 24 |
2 files changed, 31 insertions, 16 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 915dc603e..cde85a186 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4785,16 +4785,19 @@ void SmtEngine::checkModel(bool hardFailure) { } // (2) check that the value is actually a value - else if (!val.isConst()) { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: MODEL VALUE NOT A CONSTANT ***" << endl; - InternalError() - << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH " - "MODEL:" - << endl - << "model value for " << func << endl - << " is " << val << endl - << "and that is not a constant (.isConst() == false)." << endl - << "Run with `--check-models -v' for additional diagnostics."; + else if (!val.isConst()) + { + // This is only a warning since it could have been assigned an + // unevaluable term (e.g. an application of a transcendental function). + // This parallels the behavior (warnings for non-constant expressions) + // when checking whether assertions are satisfied below. + Warning() << "Warning : SmtEngine::checkModel(): " + << "model value for " << func << endl + << " is " << val << endl + << "and that is not a constant (.isConst() == false)." + << std::endl + << "Run with `--check-models -v' for additional diagnostics." + << std::endl; } // (3) check that it's the correct (sub)type diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d176b015d..e15641bb4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2268,14 +2268,26 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { Node val = getModel()->getValue(assertion); if (val != d_true) { + std::stringstream ss; + ss << theoryId + << " has an asserted fact that the model doesn't satisfy." << endl + << "The fact: " << assertion << endl + << "Model value: " << val << endl; if (hardFailure) { - InternalError() - << theoryId - << " has an asserted fact that the model doesn't satisfy." - << endl - << "The fact: " << assertion << endl - << "Model value: " << val << endl; + if (val == d_false) + { + // Always an error if it is false + InternalError() << ss.str(); + } + else + { + // Otherwise just a warning. Notice this case may happen for + // assertions with unevaluable operators, e.g. transcendental + // functions. It also may happen for separation logic, where + // check-model support is limited. + Warning() << ss.str(); + } } } } |