diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-07 20:45:13 +0000 |
commit | e568f34e1f4713c678336fbef1006e585128d466 (patch) | |
tree | a20636a5d50a84d22016f278e9f3a036436125dd /src/parser/smt2 | |
parent | d71827eef17c181d225f64ea59d26c34d76b9b1e (diff) |
LogicInfo locking implemented, and some initialization-order issues in SmtEngine resolved.
ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 37 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 28 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 2 |
3 files changed, 53 insertions, 14 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 19f77ac87..d711ddab5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -191,6 +191,7 @@ command returns [CVC4::Command* cmd = NULL] DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl; + PARSER_STATE->checkThatLogicIsSet(); unsigned arity = AntlrInput::tokenToUnsigned(n); if(arity == 0) { Type type = PARSER_STATE->mkSort(name); @@ -204,6 +205,7 @@ command returns [CVC4::Command* cmd = NULL] DEFINE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK { + PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->pushScope(); for(std::vector<std::string>::const_iterator i = names.begin(), iend = names.end(); @@ -224,6 +226,7 @@ command returns [CVC4::Command* cmd = NULL] LPAREN_TOK sortList[sorts] RPAREN_TOK sortSymbol[t,CHECK_DECLARED] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; + PARSER_STATE->checkThatLogicIsSet(); if( sorts.size() > 0 ) { t = EXPR_MANAGER->mkFunctionType(sorts, t); } @@ -235,6 +238,7 @@ command returns [CVC4::Command* cmd = NULL] sortSymbol[t,CHECK_DECLARED] { /* add variables to parser state before parsing term */ Debug("parser") << "define fun: '" << name << "'" << std::endl; + PARSER_STATE->checkThatLogicIsSet(); if( sortedVarNames.size() > 0 ) { std::vector<CVC4::Type> sorts; sorts.reserve(sortedVarNames.size()); @@ -263,13 +267,9 @@ command returns [CVC4::Command* cmd = NULL] $cmd = new DefineFunctionCommand(name, func, terms, expr); } | /* value query */ - ( GET_VALUE_TOK - { if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("Strict compliance mode doesn't recognize \"eval\". Maybe you want (get-value...)?"); - } - } ) - LPAREN_TOK termList[terms,expr] RPAREN_TOK - { if(terms.size() == 1) { + GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK + { PARSER_STATE->checkThatLogicIsSet(); + if(terms.size() == 1) { $cmd = new GetValueCommand(terms[0]); } else { CommandSequence* seq = new CommandSequence(); @@ -284,24 +284,31 @@ command returns [CVC4::Command* cmd = NULL] } | /* get-assignment */ GET_ASSIGNMENT_TOK - { cmd = new GetAssignmentCommand; } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new GetAssignmentCommand; } | /* assertion */ ASSERT_TOK term[expr] - { cmd = new AssertCommand(expr); } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new AssertCommand(expr); } | /* checksat */ CHECKSAT_TOK - { cmd = new CheckSatCommand(MK_CONST(bool(true))); } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new CheckSatCommand(MK_CONST(bool(true))); } | /* get-assertions */ GET_ASSERTIONS_TOK - { cmd = new GetAssertionsCommand; } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new GetAssertionsCommand; } | /* get-proof */ GET_PROOF_TOK - { cmd = new GetProofCommand; } + { PARSER_STATE->checkThatLogicIsSet(); + cmd = new GetProofCommand; } | /* get-unsat-core */ GET_UNSAT_CORE_TOK - { UNSUPPORTED("unsat cores not yet supported"); } + { PARSER_STATE->checkThatLogicIsSet(); + UNSUPPORTED("unsat cores not yet supported"); } | /* push */ PUSH_TOK + { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { @@ -323,6 +330,7 @@ command returns [CVC4::Command* cmd = NULL] } } ) | POP_TOK + { PARSER_STATE->checkThatLogicIsSet(); } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { @@ -348,7 +356,8 @@ command returns [CVC4::Command* cmd = NULL] /* CVC4-extended SMT-LIBv2 commands */ | extendedCommand[cmd] - { if(PARSER_STATE->strictModeEnabled()) { + { PARSER_STATE->checkThatLogicIsSet(); + if(PARSER_STATE->strictModeEnabled()) { PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3fa00baae..709ba087f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -17,6 +17,7 @@ **/ #include "expr/type.h" +#include "expr/command.h" #include "parser/parser.h" #include "parser/smt/smt.h" #include "parser/smt2/smt2.h" @@ -193,6 +194,16 @@ void Smt2::setLogic(const std::string& name) { addTheory(THEORY_REALS); break; + case Smt::ALL_SUPPORTED: + /* fall through */ + case Smt::QF_ALL_SUPPORTED: + addTheory(THEORY_ARRAYS); + addOperator(kind::APPLY_UF); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_BITVECTORS); + break; + case Smt::AUFLIA: case Smt::AUFLIRA: case Smt::AUFNIRA: @@ -211,5 +222,22 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) { // TODO: ??? } +void Smt2::checkThatLogicIsSet() { + if( ! logicIsSet() ) { + if( strictModeEnabled() ) { + parseError("set-logic must appear before this point."); + } else { + warning("No set-logic command was given before this point."); + warning("CVC4 will assume the non-standard ALL_SUPPORTED logic."); + warning("Consider setting a stricter logic for (likely) better performance."); + warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED)."); + + setLogic("ALL_SUPPORTED"); + + preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED")); + } + } +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index e9363b970..b71f63558 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -72,6 +72,8 @@ public: void setOption(const std::string& flag, const SExpr& sexpr); + void checkThatLogicIsSet(); + private: void addArithmeticOperators(); |