summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/antlr_input.cpp4
-rw-r--r--src/parser/antlr_input.h5
-rw-r--r--src/parser/input.h5
-rw-r--r--src/parser/parser.h5
-rw-r--r--src/parser/smt/smt.cpp12
-rw-r--r--src/parser/smt/smt.h4
-rw-r--r--src/parser/smt2/Smt2.g37
-rw-r--r--src/parser/smt2/smt2.cpp28
-rw-r--r--src/parser/smt2/smt2.h2
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback