summaryrefslogtreecommitdiff
path: root/src/parser/smt1
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt1')
-rw-r--r--src/parser/smt1/Smt1.g8
-rw-r--r--src/parser/smt1/smt1.cpp30
-rw-r--r--src/parser/smt1/smt1_input.cpp8
-rw-r--r--src/parser/smt1/smt1_input.h4
4 files changed, 26 insertions, 24 deletions
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index b228fb9ec..e093037eb 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -241,7 +241,7 @@ annotatedFormula[CVC4::Expr& expr]
{ if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
/* Unary AND/OR can be replaced with the argument.
It just so happens expr should already by the only argument. */
- Assert( expr == args[0] );
+ assert( expr == args[0] );
} else if( CVC4::kind::isAssociative(kind) &&
args.size() > EXPR_MANAGER->maxArity(kind) ) {
/* Special treatment for associative operators with lots of children */
@@ -474,7 +474,7 @@ functionDeclaration[CVC4::Command*& smt_command]
{ sorts.push_back(t); }
sortList[sorts] RPAREN_TOK
{ if( sorts.size() == 1 ) {
- Assert( t == sorts[0] );
+ assert( t == sorts[0] );
} else {
t = EXPR_MANAGER->mkFunctionType(sorts);
}
@@ -566,8 +566,8 @@ annotation[CVC4::Command*& smt_command]
: attribute[key]
( USER_VALUE
{ std::string value = AntlrInput::tokenText($USER_VALUE);
- Assert(*value.begin() == '{');
- Assert(*value.rbegin() == '}');
+ assert(*value.begin() == '{');
+ assert(*value.rbegin() == '}');
// trim whitespace
value.erase(value.begin(), value.begin() + 1);
value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c91743226..9074cc20a 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -117,9 +117,10 @@ void Smt1::addTheory(Theory theory) {
}
case THEORY_BITVECTOR_ARRAYS_EX: {
- Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)");
- //addOperator(kind::SELECT);
- //addOperator(kind::STORE);
+ // We don't define the "Array" symbol in this case;
+ // the parser creates the Array[m:n] types on the fly.
+ addOperator(kind::SELECT);
+ addOperator(kind::STORE);
break;
}
@@ -134,7 +135,6 @@ void Smt1::addTheory(Theory theory) {
case THEORY_INT_ARRAYS:
case THEORY_INT_ARRAYS_EX: {
defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
-
addOperator(kind::SELECT);
addOperator(kind::STORE);
break;
@@ -167,7 +167,9 @@ void Smt1::addTheory(Theory theory) {
break;
default:
- Unhandled(theory);
+ std::stringstream ss;
+ ss << "internal error: unsupported theory " << theory;
+ throw ParserException(ss.str());
}
}
@@ -229,8 +231,8 @@ void Smt1::setLogic(const std::string& name) {
addTheory(THEORY_BITVECTORS);
break;
- case QF_ABV:
- addTheory(THEORY_ARRAYS_EX);
+ case QF_ABV:// nonstandard logic
+ addTheory(THEORY_BITVECTOR_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
break;
@@ -241,18 +243,18 @@ void Smt1::setLogic(const std::string& name) {
case QF_AUFBV:
addOperator(kind::APPLY_UF);
- addTheory(THEORY_ARRAYS_EX);
+ addTheory(THEORY_BITVECTOR_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
break;
- case QF_AUFBVLIA:
+ case QF_AUFBVLIA:// nonstandard logic
addOperator(kind::APPLY_UF);
addTheory(THEORY_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
addTheory(THEORY_INTS);
break;
- case QF_AUFBVLRA:
+ case QF_AUFBVLRA:// nonstandard logic
addOperator(kind::APPLY_UF);
addTheory(THEORY_ARRAYS_EX);
addTheory(THEORY_BITVECTORS);
@@ -260,22 +262,22 @@ void Smt1::setLogic(const std::string& name) {
break;
case QF_AUFLIA:
- addTheory(THEORY_INT_ARRAYS_EX);
+ addTheory(THEORY_INT_ARRAYS_EX);// nonstandard logic
addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
break;
- case QF_AUFLIRA:
+ case QF_AUFLIRA:// nonstandard logic
addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
addTheory(THEORY_REALS);
break;
- case ALL_SUPPORTED:
+ case ALL_SUPPORTED:// nonstandard logic
addTheory(THEORY_QUANTIFIERS);
/* fall through */
- case QF_ALL_SUPPORTED:
+ case QF_ALL_SUPPORTED:// nonstandard logic
addTheory(THEORY_ARRAYS_EX);
addOperator(kind::APPLY_UF);
addTheory(THEORY_INTS);
diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp
index 4987cd793..aae990311 100644
--- a/src/parser/smt1/smt1_input.cpp
+++ b/src/parser/smt1/smt1_input.cpp
@@ -33,7 +33,7 @@ namespace parser {
Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
- AlwaysAssert( input != NULL );
+ assert( input != NULL );
d_pSmt1Lexer = Smt1LexerNew(input);
if( d_pSmt1Lexer == NULL ) {
@@ -43,7 +43,7 @@ Smt1Input::Smt1Input(AntlrInputStream& inputStream) :
setAntlr3Lexer( d_pSmt1Lexer->pLexer );
pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
- AlwaysAssert( tokenStream != NULL );
+ assert( tokenStream != NULL );
d_pSmt1Parser = Smt1ParserNew(tokenStream);
if( d_pSmt1Parser == NULL ) {
@@ -60,12 +60,12 @@ Smt1Input::~Smt1Input() {
}
Command* Smt1Input::parseCommand()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
}
Expr Smt1Input::parseExpr()
- throw (ParserException, TypeCheckingException, AssertionException) {
+ throw (ParserException, TypeCheckingException) {
return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
}
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
index 77d6f4b50..0f8a962ba 100644
--- a/src/parser/smt1/smt1_input.h
+++ b/src/parser/smt1/smt1_input.h
@@ -69,7 +69,7 @@ protected:
* @throws ParserException if an error is encountered during parsing.
*/
Command* parseCommand()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
/**
* Parse an expression from the input. Returns a null
@@ -78,7 +78,7 @@ protected:
* @throws ParserException if an error is encountered during parsing.
*/
Expr parseExpr()
- throw(ParserException, TypeCheckingException, AssertionException);
+ throw(ParserException, TypeCheckingException);
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback