diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-02 22:13:12 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-02 22:13:12 +0000 |
commit | b8a010d260c90efa5433a71dd317a03f051c2592 (patch) | |
tree | 40f716a0895d2302954b79de45893368af942723 /src/smt/smt_engine.cpp | |
parent | 6e283659af0f95505e92a1826953509537f9d216 (diff) |
* re-enable some Z3 extended commands:
declare-const
declare-funs
declare-preds
define
simplify
* don't output --help on bad options, just invite user to try --help
* Datatypes from SMT2 parser now name the tester is-cons (e.g.)
* unknown results produce models, --check-model doesn't fail hard for
incorrect unknown models. removed the assert that kept arithmetic
from producing models if it saw nonlinear
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 08fdbec95..a857351a5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1884,8 +1884,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) { Trace("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl; // Check that SAT results generate a model correctly. - if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) { - checkModel(); + if(options::checkModels() && r.asSatisfiabilityResult() != Result::UNSAT) { + checkModel(/* hard failure iff */ ! r.isUnknown()); } return r; @@ -1948,8 +1948,8 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) { Trace("smt") << "SMT query(" << e << ") ==> " << r << endl; // Check that SAT results generate a model correctly. - if(options::checkModels() && r.asSatisfiabilityResult() == Result::SAT) { - checkModel(); + if(options::checkModels() && r.asSatisfiabilityResult() != Result::UNSAT) { + checkModel(/* hard failure iff */ ! r.isUnknown()); } return r; @@ -2179,7 +2179,7 @@ Model* SmtEngine::getModel() throw(ModalException) { return d_theoryEngine->getModel(); } -void SmtEngine::checkModel() { +void SmtEngine::checkModel(bool hardFailure) { // --check-model implies --interactive, which enables the assertion list, // so we should be ok. Assert(d_assertionList != NULL, "don't have an assertion list to check in SmtEngine::checkModel()"); @@ -2285,12 +2285,17 @@ void SmtEngine::checkModel() { if(n != NodeManager::currentNM()->mkConst(true)) { Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << endl; stringstream ss; - ss << "SmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl + ss << "SmtEngine::checkModel(): " + << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl << "assertion: " << *i << endl << "simplifies to: " << n << endl << "expected `true'." << endl << "Run with `--check-models -v' for additional diagnostics."; - InternalError(ss.str()); + if(hardFailure) { + InternalError(ss.str()); + } else { + Warning() << ss.str() << endl; + } } } Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; |