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 | |
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')
-rw-r--r-- | src/parser/antlr_input.cpp | 4 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 5 | ||||
-rw-r--r-- | src/parser/input.h | 5 | ||||
-rw-r--r-- | src/parser/parser.h | 5 | ||||
-rw-r--r-- | src/parser/smt/smt.cpp | 12 | ||||
-rw-r--r-- | src/parser/smt/smt.h | 4 | ||||
-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 |
9 files changed, 87 insertions, 15 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 67d873a48..52d98435e 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -270,6 +270,10 @@ void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { } } +void AntlrInput::warning(const std::string& message) { + Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; +} + void AntlrInput::parseError(const std::string& message) throw (ParserException, AssertionException) { Debug("parser") << "Throwing exception: " diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index bdf5fe59e..84b5099fb 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -197,6 +197,11 @@ protected: pANTLR3_COMMON_TOKEN_STREAM getTokenStream(); /** + * Issue a non-fatal warning to the user with file, line, and column info. + */ + void warning(const std::string& msg); + + /** * Throws a <code>ParserException</code> with the given message. */ void parseError(const std::string& msg) diff --git a/src/parser/input.h b/src/parser/input.h index 8fa51a095..92b039eda 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -167,6 +167,11 @@ protected: throw (ParserException, TypeCheckingException, AssertionException) = 0; /** + * Issue a warning to the user, with source file, line, and column info. + */ + virtual void warning(const std::string& msg) = 0; + + /** * Throws a <code>ParserException</code> with the given message. */ virtual void parseError(const std::string& msg) diff --git a/src/parser/parser.h b/src/parser/parser.h index 405e397b8..a3ddba013 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -457,6 +457,11 @@ public: /** Parse and return the next expression. */ Expr nextExpression() throw(ParserException); + /** Issue a warning to the user. */ + inline void warning(const std::string& msg) { + d_input->warning(msg); + } + /** Raise a parse error with the given message. */ inline void parseError(const std::string& msg) throw(ParserException) { d_input->parseError(msg); diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp index b9db8dace..c3b81655c 100644 --- a/src/parser/smt/smt.cpp +++ b/src/parser/smt/smt.cpp @@ -54,6 +54,8 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL logicMap["QF_UFNIRA"] = QF_UFNIRA; logicMap["QF_AUFLIA"] = QF_AUFLIA; logicMap["QF_AUFLIRA"] = QF_AUFLIRA; + logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED; + logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED; return logicMap; } @@ -248,6 +250,16 @@ void Smt::setLogic(const std::string& name) { addTheory(THEORY_REALS); break; + case ALL_SUPPORTED: + /* fall through */ + case QF_ALL_SUPPORTED: + addTheory(THEORY_ARRAYS_EX); + addUf(); + addTheory(THEORY_INTS); + addTheory(THEORY_REALS); + addTheory(THEORY_BITVECTORS); + break; + case AUFLIA: case AUFLIRA: case AUFNIRA: diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h index 34ec624bc..d77808930 100644 --- a/src/parser/smt/smt.h +++ b/src/parser/smt/smt.h @@ -65,7 +65,9 @@ public: QF_UFNIRA, // nonstandard QF_UFNRA, UFLRA, - UFNIA + UFNIA, + QF_ALL_SUPPORTED, // nonstandard + ALL_SUPPORTED // nonstandard }; enum Theory { 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(); |