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/Smt2.g | |
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/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 37 |
1 files changed, 23 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."); } } |