diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-05 22:46:27 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-05 22:46:27 +0000 |
commit | 129dadba47447148096acd216d61f93e14539cb4 (patch) | |
tree | fd0053624ee96ee84eb35d1542d1977e40830750 /src/smt | |
parent | 4c87c0794b7e954afd090cfbf441caa0b09c3ef5 (diff) |
Bug-related:
* ITE removal fixed to be context-dependent (on UserContext).
Resolves incrementality bugs 376 and 396 (which had given wrong answers).
* some bugfixes for incrementality that Dejan found (fixes bug 394)
* fix for bug in SmtEngine::getValue() where definitions weren't respected
(partially resolves bug 411, but get-model is still broken).
* change status of microwave21.ec.minimized.smt2 (it's actually unsat, but
was labeled sat); re-enable it for "make regress"
Also:
* --check-model doesn't fail if quantified assertions don't simplify away.
* fix some examples, and the Java system test, for the disappearance of the
BoolExpr class
* add copy constructor to array type enumerator (the type enumerator
framework requires copy ctors, and the automatically-generated copy ctor
was copying pointers that were then deleted, leaving dangling pointers in
the copy and causing segfaults)
* --dump=assertions now implies --dump=skolems
* --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow
you to dump before/after a particular preprocessing pass. E.g.,
--dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning.
"--dump=assertions" by itself is after all preprocessing, just before CNF
conversion.
* minor fixes to dumping output
* include Model in language bindings
Minor refactoring/misc:
* fix compiler warning in src/theory/model.cpp
* remove unnecessary SmtEngine::printModel().
* mkoptions script doesn't give progress output if stdout isn't a terminal
(e.g., if it's written to a log, or piped through less(1), or whatever).
* add some type enumerator unit tests
* de-emphasize --parse-only and --preprocess-only (they aren't really "common"
options)
* fix some exception throw() specifications in SmtEngine
* minor documentation clarifications
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/options_handlers.h | 51 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 200 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 22 |
3 files changed, 174 insertions, 99 deletions
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index 7d5dd56c9..2af826d24 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -75,23 +75,20 @@ benchmark\n\ declarations\n\ + Dump user declarations. Implied by all following modes.\n\ \n\ -assertions\n\ -+ Output the assertions after non-clausal simplification and static\n\ - learning phases, but before presolve-time T-lemmas arrive. If\n\ - non-clausal simplification and static learning are off\n\ - (--simplification=none --no-static-learning), the output\n\ - will closely resemble the input (with term-level ITEs removed).\n\ -\n\ skolems\n\ + Dump internally-created skolem variable declarations. These can\n\ arise from preprocessing simplifications, existential elimination,\n\ and a number of other things. Implied by all following modes.\n\ \n\ -learned\n\ -+ Output the assertions after non-clausal simplification, static\n\ - learning, and presolve-time T-lemmas. This should include all eager\n\ - T-lemmas (in the form provided by the theory, which my or may not be\n\ - clausal). Also includes level-0 BCP done by Minisat.\n\ +assertions\n\ ++ Output the assertions after preprocessing and before clausification.\n\ + Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ + where PASS is one of the preprocessing passes: skolem-quant simplify\n\ + static-learning ite-removal repeat-simplify theory-preprocessing.\n\ + PASS can also be the special value \"everything\", in which case the\n\ + assertions are printed before any preprocessing (with\n\ + \"assertions:pre-everything\") or after all preprocessing completes\n\ + (with \"assertions:post-everything\").\n\ \n\ clauses\n\ + Do all the preprocessing outlined above, and dump the CNF-converted\n\ @@ -127,7 +124,7 @@ theory::fullcheck [non-stateful]\n\ + Output completeness queries for all full-check effort-level theory checks\n\ \n\ Dump modes can be combined with multiple uses of --dump. Generally you want\n\ -one from the assertions category (either assertions, learned, or clauses), and\n\ +one from the assertions category (either assertions or clauses), and\n\ perhaps one or more stateful or non-stateful modes for checking correctness\n\ and completeness of decision procedure implementations. Stateful modes dump\n\ the contextual assertions made by the core solver (all decisions and\n\ @@ -177,8 +174,30 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { if(!strcmp(optargPtr, "benchmark")) { } else if(!strcmp(optargPtr, "declarations")) { } else if(!strcmp(optargPtr, "assertions")) { + Dump.on("assertions:post-everything"); + } else if(!strncmp(optargPtr, "assertions:", 11)) { + const char* p = optargPtr + 11; + if(!strncmp(p, "pre-", 4)) { + p += 4; + } else if(!strncmp(p, "post-", 5)) { + p += 5; + } else { + throw OptionException(std::string("don't know how to dump `") + + optargPtr + "'. Please consult --dump help."); + } + if(!strcmp(p, "everything")) { + } else if(!strcmp(p, "skolem-quant")) { + } else if(!strcmp(p, "simplify")) { + } else if(!strcmp(p, "static-learning")) { + } else if(!strcmp(p, "ite-removal")) { + } else if(!strcmp(p, "repeat-simplify")) { + } else if(!strcmp(p, "theory-preprocessing")) { + } else { + throw OptionException(std::string("don't know how to dump `") + + optargPtr + "'. Please consult --dump help."); + } + Dump.on("assertions"); } else if(!strcmp(optargPtr, "skolems")) { - } else if(!strcmp(optargPtr, "learned")) { } else if(!strcmp(optargPtr, "clauses")) { } else if(!strcmp(optargPtr, "t-conflicts") || !strcmp(optargPtr, "t-lemmas") || @@ -225,7 +244,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { Dump.on("benchmark"); if(strcmp(optargPtr, "benchmark")) { Dump.on("declarations"); - if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "assertions")) { + if(strcmp(optargPtr, "declarations")) { Dump.on("skolems"); } } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2d83b7960..0a5270d83 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5,7 +5,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): cconway, kshitij ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -199,10 +199,17 @@ class SmtEnginePrivate : public NodeManagerListener { /** Assertions to push to sat */ vector<Node> d_assertionsToCheck; - /** Map from skolem variables to index in d_assertionsToCheck containing - * corresponding introduced Boolean ite */ + /** + * Map from skolem variables to index in d_assertionsToCheck containing + * corresponding introduced Boolean ite + */ IteSkolemMap d_iteSkolemMap; +public: + /** Instance of the ITE remover */ + RemoveITE d_iteRemover; + +private: /** The top level substitutions */ SubstitutionMap d_topLevelSubstitutions; @@ -261,17 +268,17 @@ class SmtEnginePrivate : public NodeManagerListener { */ bool simplifyAssertions() throw(TypeCheckingException); - /** - * contains quantifiers - */ - bool containsQuantifiers( Node n ); - public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), + d_assertionsToPreprocess(), d_nonClausalLearnedLiterals(), + d_realAssertionsEnd(0), d_propagator(d_nonClausalLearnedLiterals, true, true), + d_assertionsToCheck(), + d_iteSkolemMap(), + d_iteRemover(smt.d_userContext), d_topLevelSubstitutions(smt.d_userContext), d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) { d_smt.d_nodeManager->subscribeEvents(this); @@ -339,6 +346,8 @@ public: d_assertionsToPreprocess.clear(); d_nonClausalLearnedLiterals.clear(); d_assertionsToCheck.clear(); + d_realAssertionsEnd = 0; + d_iteSkolemMap.clear(); } /** @@ -404,7 +413,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) - d_theoryEngine = new TheoryEngine(d_context, d_userContext, const_cast<const LogicInfo&>(d_logic)); + d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic)); // Add the theories #ifdef CVC4_FOR_EACH_THEORY_STATEMENT @@ -593,9 +602,9 @@ void SmtEngine::setLogicInternal() throw() { // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) { - Theory::setTheoryOfMode(theory::THEORY_OF_TERM_BASED); + Theory::setTheoryOfMode(THEORY_OF_TERM_BASED); } else { - Theory::setTheoryOfMode(theory::THEORY_OF_TYPE_BASED); + Theory::setTheoryOfMode(THEORY_OF_TYPE_BASED); } } else { Theory::setTheoryOfMode(options::theoryOfMode()); @@ -791,6 +800,8 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) d_logic = value.getValue(); setLogicInternal(); return; + } else { + throw UnrecognizedOptionException(); } } } @@ -800,10 +811,18 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) key == "source" || key == "category" || key == "difficulty" || - key == "smt-lib-version" || key == "notes") { // ignore these return; + } else if(key == "smt-lib-version") { + if( (value.isInteger() && value.getIntegerValue() == Integer(2)) || + (value.isRational() && value.getRationalValue() == Rational(2)) || + (value.getValue() == "2") ) { + // supported SMT-LIB version + return; + } + Warning() << "Warning: unsupported smt-lib-version: " << value << endl; + throw UnrecognizedOptionException(); } else if(key == "status") { string s; if(value.isAtom()) { @@ -1013,6 +1032,20 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF } } +// check if the given node contains a universal quantifier +static bool containsQuantifiers(Node n) { + if(n.getKind() == kind::FORALL) { + return true; + } else { + for(unsigned i = 0; i < n.getNumChildren(); ++i) { + if(containsQuantifiers(n[i])) { + return true; + } + } + return false; + } +} + Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){ Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << std::endl; if( n.getKind()==kind::NOT ){ @@ -1117,7 +1150,7 @@ void SmtEnginePrivate::removeITEs() { Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl; // Remove all of the ITE occurrences and normalize - RemoveITE::run(d_assertionsToCheck, d_iteSkolemMap); + d_iteRemover.run(d_assertionsToCheck, d_iteSkolemMap); for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]); } @@ -1144,6 +1177,18 @@ void SmtEnginePrivate::staticLearning() { } } +// do dumping (before/after any preprocessing pass) +static void dumpAssertions(const char* key, + const std::vector<Node>& assertionList) { + if( Dump.isOn("assertions") && + Dump.isOn(std::string("assertions:") + key) ) { + // Push the simplified assertions to the dump output stream + for(unsigned i = 0; i < assertionList.size(); ++ i) { + TNode n = assertionList[i]; + Dump("assertions") << AssertCommand(Expr(n.toExpr())); + } + } +} // returns false if it learns a conflict bool SmtEnginePrivate::nonClausalSimplify() { @@ -1335,7 +1380,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { NodeBuilder<> learnedBuilder(kind::AND); Assert(d_realAssertionsEnd <= d_assertionsToCheck.size()); - learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd-1]; + learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1]; if( options::incrementalSolving() || options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) { @@ -1398,7 +1443,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { } if(learnedBuilder.getNumChildren() > 1) { - d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(learnedBuilder)); + d_assertionsToCheck[d_realAssertionsEnd - 1] = + Rewriter::rewrite(Node(learnedBuilder)); } d_propagator.finish(); @@ -1544,8 +1590,11 @@ bool SmtEnginePrivate::simplifyAssertions() Trace("simplify") << "SmtEnginePrivate::simplify(): " << " doing repeated simplification" << std::endl; d_assertionsToCheck.swap(d_assertionsToPreprocess); + Assert(d_assertionsToCheck.empty()); bool noConflict = nonClausalSimplify(); - if(!noConflict) return false; + if(!noConflict) { + return false; + } } Trace("smt") << "POST repeatSimp" << std::endl; @@ -1566,20 +1615,6 @@ bool SmtEnginePrivate::simplifyAssertions() return true; } - -bool SmtEnginePrivate::containsQuantifiers( Node n ){ - if( n.getKind()==kind::FORALL ){ - return true; - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( containsQuantifiers( n[i] ) ){ - return true; - } - } - return false; - } -} - Result SmtEngine::check() { Assert(d_fullyInited); Assert(d_pendingPops == 0); @@ -1636,14 +1671,21 @@ void SmtEnginePrivate::processAssertions() { Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); + // Dump the assertions + dumpAssertions("pre-everything", d_assertionsToPreprocess); + Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - // any assertions added beyond realAssertionsEnd must NOT affect the equisatisfiability + Assert(d_assertionsToCheck.size() == 0); + + // any assertions added beyond realAssertionsEnd must NOT affect the + // equisatisfiability d_realAssertionsEnd = d_assertionsToPreprocess.size(); - if (d_realAssertionsEnd == 0) { + if(d_realAssertionsEnd == 0) { + // nothing to do return; } @@ -1682,6 +1724,7 @@ void SmtEnginePrivate::processAssertions() { Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl; } + dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); if( options::preSkolemQuant() ){ //apply pre-skolemization to existential quantifiers for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { @@ -1694,10 +1737,14 @@ void SmtEnginePrivate::processAssertions() { } } } + dumpAssertions("post-skolem-quant", d_assertionsToPreprocess); + dumpAssertions("pre-simplify", d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; bool noConflict = simplifyAssertions(); + dumpAssertions("post-simplify", d_assertionsToPreprocess); + dumpAssertions("pre-static-learning", d_assertionsToCheck); if(options::doStaticLearning()) { // Perform static learning Chat() << "doing static learning..." << endl; @@ -1705,7 +1752,9 @@ void SmtEnginePrivate::processAssertions() { << "performing static learning" << endl; staticLearning(); } + dumpAssertions("post-static-learning", d_assertionsToCheck); + dumpAssertions("pre-ite-removal", d_assertionsToCheck); { Chat() << "removing term ITEs..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime); @@ -1714,7 +1763,9 @@ void SmtEnginePrivate::processAssertions() { removeITEs(); d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size(); } + dumpAssertions("post-ite-removal", d_assertionsToCheck); + dumpAssertions("pre-repeat-simplify", d_assertionsToCheck); if(options::repeatSimp()) { d_assertionsToCheck.swap(d_assertionsToPreprocess); Chat() << "simplifying assertions..." << endl; @@ -1725,7 +1776,7 @@ void SmtEnginePrivate::processAssertions() { IteSkolemMap::iterator it = d_iteSkolemMap.begin(); IteSkolemMap::iterator iend = d_iteSkolemMap.end(); NodeBuilder<> builder(kind::AND); - builder << d_assertionsToCheck[d_realAssertionsEnd-1]; + builder << d_assertionsToCheck[d_realAssertionsEnd - 1]; for (; it != iend; ++it) { if (d_topLevelSubstitutions.hasSubstitution((*it).first)) { builder << d_assertionsToCheck[(*it).second]; @@ -1733,7 +1784,8 @@ void SmtEnginePrivate::processAssertions() { } } if(builder.getNumChildren() > 1) { - d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(builder)); + d_assertionsToCheck[d_realAssertionsEnd - 1] = + Rewriter::rewrite(Node(builder)); } // For some reason this is needed for some benchmarks, such as // http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 @@ -1742,6 +1794,7 @@ void SmtEnginePrivate::processAssertions() { // Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); } } + dumpAssertions("post-repeat-simplify", d_assertionsToCheck); // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones @@ -1756,6 +1809,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; + dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck); { Chat() << "theory preprocessing..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime); @@ -1765,14 +1819,7 @@ void SmtEnginePrivate::processAssertions() { d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]); } } - - if(Dump.isOn("assertions")) { - // Push the simplified assertions to the dump output stream - for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - Dump("assertions") - << AssertCommand(d_assertionsToCheck[i].toExpr()); - } - } + dumpAssertions("post-theory-preprocessing", d_assertionsToCheck); // Push the formula to decision engine if(noConflict) { @@ -1785,6 +1832,8 @@ void SmtEnginePrivate::processAssertions() { // end: INVARIANT to maintain: no reordering of assertions or // introducing new ones + dumpAssertions("post-everything", d_assertionsToCheck); + // Push the formula to SAT { Chat() << "converting to CNF..." << endl; @@ -1824,7 +1873,7 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { } } -Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) { +Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException, ModalException) { Assert(e.isNull() || e.getExprManager() == d_exprManager); @@ -1891,7 +1940,7 @@ Result SmtEngine::checkSat(const Expr& e) throw(TypeCheckingException) { return r; }/* SmtEngine::checkSat() */ -Result SmtEngine::query(const Expr& e) throw(TypeCheckingException) { +Result SmtEngine::query(const Expr& e) throw(TypeCheckingException, ModalException) { Assert(!e.isNull()); Assert(e.getExprManager() == d_exprManager); @@ -2003,8 +2052,7 @@ Expr SmtEngine::expandDefinitions(const Expr& e) throw(TypeCheckingException) { return d_private->expandDefinitions(Node::fromExpr(e), cache).toExpr(); } -Expr SmtEngine::getValue(const Expr& e) - throw(ModalException) { +Expr SmtEngine::getValue(const Expr& e) throw(ModalException) { Assert(e.getExprManager() == d_exprManager); SmtScope smts(this); @@ -2028,13 +2076,15 @@ Expr SmtEngine::getValue(const Expr& e) throw ModalException(msg); } - // do not need to apply preprocessing substitutions (should be recorded in model already) + // do not need to apply preprocessing substitutions (should be recorded + // in model already) - // Normalize for the theories - Node n = Rewriter::rewrite( e.getNode() ); + // Expand, then normalize + Node n = expandDefinitions(e).getNode(); + n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; - theory::TheoryModel* m = d_theoryEngine->getModel(); + TheoryModel* m = d_theoryEngine->getModel(); Node resultNode; if( m ){ resultNode = m->getValue( n ); @@ -2112,7 +2162,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { Node n = Rewriter::rewrite(*i); Trace("smt") << "--- getting value of " << n << endl; - theory::TheoryModel* m = d_theoryEngine->getModel(); + TheoryModel* m = d_theoryEngine->getModel(); Node resultNode; if( m ){ resultNode = m->getValue( n ); @@ -2192,15 +2242,19 @@ void SmtEngine::checkModel(bool hardFailure) { // and if Notice() is on, the user gave --verbose (or equivalent). Notice() << "SmtEngine::checkModel(): generating model" << endl; - theory::TheoryModel* m = d_theoryEngine->getModel(); + TheoryModel* m = d_theoryEngine->getModel(); if(Notice.isOn()) { - printModel(Notice.getStream(), m); + // This operator<< routine is non-const (i.e., takes a non-const Model&). + // This confuses the Notice() output routines, so extract the ostream + // from it and output it "manually." Should be fixed by making Model + // accessors const. + Notice.getStream() << *m; } // We have a "fake context" for the substitution map (we don't need it // to be context-dependent) context::Context fakeContext; - theory::SubstitutionMap substitutions(&fakeContext); + SubstitutionMap substitutions(&fakeContext); for(size_t k = 0; k < m->getNumCommands(); ++k) { const DeclareFunctionCommand* c = dynamic_cast<const DeclareFunctionCommand*>(m->getCommand(k)); @@ -2239,7 +2293,7 @@ void SmtEngine::checkModel(bool hardFailure) { // now check if n contains func by doing a substitution // [func->func2] and checking equality of the Nodes. // (this just a way to check if func is in n.) - theory::SubstitutionMap subs(&fakeContext); + SubstitutionMap subs(&fakeContext); Node func2 = NodeManager::currentNM()->mkSkolem("", TypeNode::fromType(func.getType()), "", NodeManager::SKOLEM_NO_NOTIFY); subs.addSubstitution(func, func2); if(subs.apply(n) != n) { @@ -2281,9 +2335,22 @@ void SmtEngine::checkModel(bool hardFailure) { n = Node::fromExpr(simplify(n.toExpr())); Notice() << "SmtEngine::checkModel(): -- simplifies to " << n << endl; + TheoryId thy = Theory::theoryOf(n); + if(thy == THEORY_QUANTIFIERS || thy == THEORY_REWRITERULES) { + // Note this "skip" is done here, rather than above. This is + // because (1) the quantifier could in principle simplify to false, + // which should be reported, and (2) checking for the quantifier + // above, before simplification, doesn't catch buried quantifiers + // anyway (those not at the top-level). + Notice() << "SmtEngine::checkModel(): -- skipping quantified assertion" + << endl; + continue; + } + // The result should be == true. if(n != NodeManager::currentNM()->mkConst(true)) { - Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" << endl; + Notice() << "SmtEngine::checkModel(): *** PROBLEM: EXPECTED `TRUE' ***" + << endl; stringstream ss; ss << "SmtEngine::checkModel(): " << "ERRORS SATISFYING ASSERTIONS WITH MODEL:" << endl @@ -2328,8 +2395,7 @@ Proof* SmtEngine::getProof() throw(ModalException) { #endif /* CVC4_PROOF */ } -vector<Expr> SmtEngine::getAssertions() - throw(ModalException) { +vector<Expr> SmtEngine::getAssertions() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); if(Dump.isOn("benchmark")) { @@ -2346,7 +2412,7 @@ vector<Expr> SmtEngine::getAssertions() return vector<Expr>(d_assertionList->begin(), d_assertionList->end()); } -void SmtEngine::push() { +void SmtEngine::push() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -2371,7 +2437,7 @@ void SmtEngine::push() { << d_userContext->getLevel() << endl; } -void SmtEngine::pop() { +void SmtEngine::pop() throw(ModalException) { SmtScope smts(this); finalOptionsAreSet(); Trace("smt") << "SMT pop()" << endl; @@ -2415,7 +2481,7 @@ void SmtEngine::internalPush() { if(options::incrementalSolving()) { d_private->processAssertions(); d_userContext->push(); - d_context->push(); + // the d_context push is done inside of the SAT solver d_propEngine->push(); } } @@ -2435,7 +2501,7 @@ void SmtEngine::doPendingPops() { Assert(d_pendingPops == 0 || options::incrementalSolving()); while(d_pendingPops > 0) { d_propEngine->pop(); - d_context->pop(); + // the d_context pop is done inside of the SAT solver d_userContext->pop(); --d_pendingPops; } @@ -2503,15 +2569,9 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() { return d_statisticsRegistry->getStatistic(name); } -void SmtEngine::printModel( std::ostream& out, Model* m ){ - SmtScope smts(this); - Expr::dag::Scope scope(out, false); - Printer::getPrinter(options::outputLanguage())->toStream( out, m ); -} - -void SmtEngine::setUserAttribute( std::string& attr, Expr expr ){ +void SmtEngine::setUserAttribute(std::string& attr, Expr expr) { SmtScope smts(this); - d_theoryEngine->setUserAttribute( attr, expr.getNode() ); + d_theoryEngine->setUserAttribute(attr, expr.getNode()); } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index df2e47b5b..3ede00510 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -290,8 +290,8 @@ class CVC4_PUBLIC SmtEngine { smt::SmtEngineStatistics* d_stats; /** - * Add to Model command. This is used for recording a command that should be reported - * during a get-model call. + * Add to Model command. This is used for recording a command + * that should be reported during a get-model call. */ void addToModelCommand(Command* c); @@ -369,13 +369,13 @@ public: * of assertions by asserting the query expression's negation and * calling check(). Returns valid, invalid, or unknown result. */ - Result query(const Expr& e) throw(TypeCheckingException); + Result query(const Expr& e) throw(TypeCheckingException, ModalException); /** * Assert a formula (if provided) to the current context and call * check(). Returns sat, unsat, or unknown result. */ - Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException); + Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException); /** * Simplify a formula without doing "much" work. Does not involve @@ -442,12 +442,12 @@ public: /** * Push a user-level context. */ - void push(); + void push() throw(ModalException); /** * Pop a user-level context. Throws an exception if nothing to pop. */ - void pop(); + void pop() throw(ModalException); /** * Interrupt a running query. This can be called from another thread @@ -572,14 +572,10 @@ public: } /** - * print model function (need this?) + * Set user attribute. + * This function is called when an attribute is set by a user. + * In SMT-LIBv2 this is done via the syntax (! expr :attr) */ - void printModel( std::ostream& out, Model* m ); - - /** Set user attribute - * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done - * via the syntax (! expr :attr) - */ void setUserAttribute( std::string& attr, Expr expr ); };/* class SmtEngine */ |