From b8a010d260c90efa5433a71dd317a03f051c2592 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 2 Oct 2012 22:13:12 +0000 Subject: [PATCH] * 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.) --- RELEASE-NOTES | 8 +- src/main/main.cpp | 5 +- src/parser/smt2/Smt2.g | 117 +++++++++++++++++++++++++++++- src/smt/smt_engine.cpp | 19 +++-- src/smt/smt_engine.h | 2 +- src/theory/arith/theory_arith.cpp | 2 +- 6 files changed, 135 insertions(+), 18 deletions(-) diff --git a/RELEASE-NOTES b/RELEASE-NOTES index 9eadf916a..9ad246a9c 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -28,8 +28,9 @@ but may produce strange results. For example: COUNTEREXAMPLE; % f : (INT) -> INT = LAMBDA(x1:INT) : 0; -CVC3 can be used to produce TCCs for this input (with the +dump-tcc option), -and the TCC can be checked with CVC4. +CVC3 can be used to produce TCCs for this input (with the +dump-tcc option). +The TCC can be checked by CVC3 or another solver. (CVC3 can also check +TCCs while solving with +tcc.) ** Changes in CVC's Presentation Language @@ -75,7 +76,8 @@ processed. ** Getting statistics -Statistics can be dumped on exit (both normal and abnormal exits) +Statistics can be dumped on exit (both normal and abnormal exits) with +the --statistics command line option. ** Time and resource limits diff --git a/src/main/main.cpp b/src/main/main.cpp index e3196bb4e..9fa1db7bc 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -59,8 +59,9 @@ int main(int argc, char* argv[]) { #ifdef CVC4_COMPETITION_MODE *opts[options::out] << "unknown" << endl; #endif - cerr << "CVC4 Error:" << endl << e << endl; - printUsage(opts); + cerr << "CVC4 Error:" << endl << e << endl << endl + << "Please use --help to get help on command-line options." + << endl; } catch(Exception& e) { #ifdef CVC4_COMPETITION_MODE *opts[options::out] << "unknown" << endl; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1b778f87a..37b926c34 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -375,7 +375,9 @@ extendedCommand[CVC4::Command*& cmd] SExpr sexpr; std::string name; std::vector names; + std::vector terms; std::vector sorts; + std::vector > sortedVarNames; } /* Extended SMT-LIBv2 set of commands syntax, not permitted in * --smtlib2 compliance mode. */ @@ -388,7 +390,7 @@ extendedCommand[CVC4::Command*& cmd] cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } | /* get model */ GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetModelCommand; } + { cmd = new GetModelCommand; } | ECHO_TOK ( simpleSymbolicExpr[sexpr] { std::stringstream ss; @@ -398,6 +400,107 @@ extendedCommand[CVC4::Command*& cmd] | { cmd = new EchoCommand(); } ) | rewriterulesCommand[cmd] + + /* Support some of Z3's extended SMT-LIBv2 commands */ + + | DECLARE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + { Expr c = PARSER_STATE->mkVar(name, t); + $cmd = new DeclareFunctionCommand(name, c, t); } + + | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { $cmd = new CommandSequence(); } + LPAREN_TOK + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] + { PARSER_STATE->checkUserSymbol(name); + Type type = PARSER_STATE->mkSort(name); + static_cast($cmd)->addCommand(new DeclareTypeCommand(name, 0, type)); + } + )+ + RPAREN_TOK + + | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { $cmd = new CommandSequence(); } + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + nonemptySortList[sorts] RPAREN_TOK + { Type t; + if(sorts.size() > 1) { + t = EXPR_MANAGER->mkFunctionType(sorts); + } else { + t = sorts[0]; + } + Expr func = PARSER_STATE->mkVar(name, t); + static_cast($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + } + )+ + RPAREN_TOK + + | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); } + { $cmd = new CommandSequence(); } + LPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortList[sorts] RPAREN_TOK + { Type t = EXPR_MANAGER->booleanType(); + if(sorts.size() > 0) { + t = EXPR_MANAGER->mkFunctionType(sorts, t); + } + Expr func = PARSER_STATE->mkVar(name, t); + static_cast($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + } + )+ + RPAREN_TOK + + | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); } + ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + term[e,e2] + { Expr func = PARSER_STATE->mkFunction(name, e.getType()); + $cmd = new DefineFunctionCommand(name, func, e); + } + | LPAREN_TOK + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortedVarList[sortedVarNames] RPAREN_TOK + { /* add variables to parser state before parsing term */ + Debug("parser") << "define fun: '" << name << "'" << std::endl; + PARSER_STATE->pushScope(); + for(std::vector >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second)); + } + } + term[e,e2] + { PARSER_STATE->popScope(); + // declare the name down here (while parsing term, signature + // must not be extended with the name itself; no recursion + // permitted) + Type t = e.getType(); + if( sortedVarNames.size() > 0 ) { + std::vector sorts; + sorts.reserve(sortedVarNames.size()); + for(std::vector >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + sorts.push_back((*i).second); + } + t = EXPR_MANAGER->mkFunctionType(sorts, t); + } + Expr func = PARSER_STATE->mkFunction(name, t); + $cmd = new DefineFunctionCommand(name, func, terms, e); + } + ) + + | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } + term[e,e2] + { cmd = new SimplifyCommand(e); } ; rewriterulesCommand[CVC4::Command*& cmd] @@ -801,7 +904,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] Expr e2; } : KEYWORD - { + { attr = AntlrInput::tokenText($KEYWORD); //EXPR_MANAGER->setNamedAttribute( expr, attr ); if( attr==":rewrite-rule" ){ @@ -823,7 +926,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] retExpr = MK_EXPR(kind::INST_PATTERN, patexprs); } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] - { + { attr = std::string(":named"); std::string name = sexpr.getValue(); // FIXME ensure expr is a closed subterm @@ -1160,7 +1263,7 @@ constructorDef[CVC4::Datatype& type] } : symbol[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester - std::string testerId("is_"); + std::string testerId("is-"); testerId.append(id); PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); ctor = new CVC4::DatatypeConstructor(id, testerId); @@ -1218,6 +1321,12 @@ ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; REDUCTION_RULE_TOK : 'assert-reduction'; PROPAGATION_RULE_TOK : 'assert-propagation'; +DECLARE_SORTS_TOK : 'declare-sorts'; +DECLARE_FUNS_TOK : 'declare-funs'; +DECLARE_PREDS_TOK : 'declare-preds'; +DEFINE_TOK : 'define'; +DECLARE_CONST_TOK : 'declare-const'; +SIMPLIFY_TOK : 'simplify'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; 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; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index fb456a4a4..096708f53 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -219,7 +219,7 @@ class CVC4_PUBLIC SmtEngine { * Check that a generated Model (via getModel()) actually satisfies * all user assertions. */ - void checkModel(); + void checkModel(bool hardFailure = true); /** * This is something of an "init" procedure, but is idempotent; call diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 17c2b51f3..f8f0756c7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2075,7 +2075,7 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) { void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ AlwaysAssert(d_qflraStatus == Result::SAT); - AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); + //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; -- 2.30.2