diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 48 |
1 files changed, 38 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 19bfe3ca5..d0a920653 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -603,7 +603,9 @@ public: val = d_smt.d_nodeManager->mkAbstractValue(n.getType()); d_abstractValueMap.addSubstitution(val, n); } - return val; + // We are supposed to ascribe types to all abstract values that go out. + Node retval = d_smt.d_nodeManager->mkNode(kind::APPLY_TYPE_ASCRIPTION, d_smt.d_nodeManager->mkConst(AscriptionType(n.getType().toType())), val); + return retval; } std::hash_map<Node, Node, NodeHashFunction> rewriteApplyToConstCache; @@ -675,6 +677,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_modelCommands(NULL), d_dumpCommands(), d_logic(), + d_originalOptions(em->getOptions()), d_pendingPops(0), d_fullyInited(false), d_problemExtended(false), @@ -737,7 +740,7 @@ void SmtEngine::finishInit() { // cleanup ordering issue and Nodes/TNodes. If SAT is popped // first, some user-context-dependent TNodes might still exist // with rc == 0. - if(options::interactive() || + if(options::produceAssertions() || options::incrementalSolving()) { // In the case of incremental solving, we appear to need these to // ensure the relevant Nodes remain live. @@ -961,9 +964,9 @@ void SmtEngine::setDefaults() { } if(options::checkModels()) { - if(! options::interactive()) { - Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; - setOption("interactive-mode", SExpr("true")); + if(! options::produceAssertions()) { + Notice() << "SmtEngine: turning on produce-assertions to support check-models" << endl; + setOption("produce-assertions", SExpr("true")); } } @@ -1450,8 +1453,23 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } else if(key == "smt-lib-version") { if( (value.isInteger() && value.getIntegerValue() == Integer(2)) || (value.isRational() && value.getRationalValue() == Rational(2)) || - (value.getValue() == "2") ) { + value.getValue() == "2" || + value.getValue() == "2.0" ) { // supported SMT-LIB version + if(!options::outputLanguage.wasSetByUser() && + options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) { + options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0); + *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0); + } + return; + } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) || + value.getValue() == "2.5" ) { + // supported SMT-LIB version + if(!options::outputLanguage.wasSetByUser() && + options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) { + options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5); + *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5); + } return; } Warning() << "Warning: unsupported smt-lib-version: " << value << endl; @@ -1530,6 +1548,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const throw ModalException("Can't get-info :reason-unknown when the " "last result wasn't unknown!"); } + } else if(key == "assertion-stack-levels") { + return SExpr(d_userLevels.size()); } else if(key == "all-options") { // get the options, like all-statistics return Options::current().getOptions(); @@ -3660,6 +3680,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin if(options::abstractValues() && resultNode.getType().isArray()) { resultNode = d_private->mkAbstractValue(resultNode); + Trace("smt") << "--- abstract value >> " << resultNode << endl; } return resultNode.toExpr(); @@ -3824,8 +3845,8 @@ Model* SmtEngine::getModel() throw(ModalException) { } void SmtEngine::checkModel(bool hardFailure) { - // --check-model implies --interactive, which enables the assertion list, - // so we should be ok. + // --check-model implies --produce-assertions, 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()"); TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); @@ -4070,9 +4091,9 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException) { Dump("benchmark") << GetAssertionsCommand(); } Trace("smt") << "SMT getAssertions()" << endl; - if(!options::interactive()) { + if(!options::produceAssertions()) { const char* msg = - "Cannot query the current assertion list when not in interactive mode."; + "Cannot query the current assertion list when not in produce-assertions mode."; throw ModalException(msg); } Assert(d_assertionList != NULL); @@ -4196,13 +4217,20 @@ void SmtEngine::reset() throw() { if(Dump.isOn("benchmark")) { Dump("benchmark") << ResetCommand(); } + Options opts = d_originalOptions; this->~SmtEngine(); + NodeManager::fromExprManager(em)->getOptions() = opts; new(this) SmtEngine(em); } void SmtEngine::resetAssertions() throw() { SmtScope smts(this); + Trace("smt") << "SMT resetAssertions()" << endl; + if(Dump.isOn("benchmark")) { + Dump("benchmark") << ResetAssertionsCommand(); + } + while(!d_userLevels.empty()) { pop(); } |