summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_template.cpp6
-rw-r--r--src/expr/expr_template.h8
-rw-r--r--src/expr/node.cpp8
-rw-r--r--src/expr/node.h11
-rw-r--r--src/parser/cvc/Cvc.g148
-rw-r--r--src/parser/parser_exception.h10
-rw-r--r--src/printer/cvc/cvc_printer.cpp15
-rw-r--r--src/smt/smt_engine.cpp24
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h8
-rw-r--r--src/util/exception.h34
-rw-r--r--src/util/language.h21
-rw-r--r--test/regress/regress0/bv/Makefile.am2
-rw-r--r--test/system/ouroborous.cpp81
13 files changed, 229 insertions, 147 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 51a734757..74bfd3f2b 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -72,10 +72,8 @@ TypeCheckingException::~TypeCheckingException() throw () {
delete d_expr;
}
-std::string TypeCheckingException::toString() const {
- std::stringstream ss;
- ss << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
- return ss.str();
+void TypeCheckingException::toStream(std::ostream& os) const {
+ os << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr;
}
Expr TypeCheckingException::getExpression() const {
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index c45cc9b99..291016044 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -99,8 +99,12 @@ public:
*/
Expr getExpression() const;
- /** Returns the message corresponding to the type-checking failure */
- std::string toString() const;
+ /**
+ * Returns the message corresponding to the type-checking failure.
+ * We prefer toStream() to toString() because that keeps the expr-depth
+ * and expr-language settings present in the stream.
+ */
+ void toStream(std::ostream& out) const;
friend class ExprManager;
};/* class TypeCheckingException */
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 445d91da8..586d0cb13 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -5,7 +5,7 @@
** Major contributors: dejan
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -35,10 +35,8 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
delete d_node;
}
-string TypeCheckingExceptionPrivate::toString() const {
- stringstream ss;
- ss << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
- return ss.str();
+void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const {
+ os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
}
Node TypeCheckingExceptionPrivate::getNode() const {
diff --git a/src/expr/node.h b/src/expr/node.h
index 6fe1e7d0e..a40b3fce5 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -80,9 +80,14 @@ public:
*/
NodeTemplate<true> getNode() const;
- /** Returns the message corresponding to the type-checking failure */
- std::string toString() const;
-};
+ /**
+ * Returns the message corresponding to the type-checking failure.
+ * We prefer toStream() to toString() because that keeps the expr-depth
+ * and expr-language settings present in the stream.
+ */
+ void toStream(std::ostream& out) const;
+
+};/* class TypeCheckingExceptionPrivate */
/**
* \typedef NodeTemplate<true> Node;
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 792f53605..794f0a670 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -460,8 +460,8 @@ command returns [CVC4::Command* cmd = 0]
std::vector<CVC4::Datatype> dts;
Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); }
- | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); }
+ : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); }
+ | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); }
| CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
| CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_CONST(true)); }
| OPTION_TOK STRING_LITERAL symbolicExpr[sexpr] SEMICOLON
@@ -684,7 +684,16 @@ identifier[std::string& id,
;
/**
- * Match the type in a declaration and do the declaration binding.
+ * Match the type in a declaration and do the declaration binding. If
+ * "check" is CHECK_NONE, then identifiers occurring in the type need
+ * not exist! They are created as "unresolved" types and linked up in
+ * a type-substitution pass. Right now, only datatype definitions are
+ * supported in this way (since type names can occur without any
+ * forward-declaration in CVC language datatype definitions, we have
+ * to create types for them on-the-fly). Before passing CHECK_NONE
+ * you really should have a clear idea of WHY you need to parse that
+ * way; then you should trace through Parser::mkMutualDatatypeType()
+ * to figure out just what you're in for.
*/
type[CVC4::Type& t,
CVC4::parser::DeclarationCheck check]
@@ -1059,8 +1068,8 @@ concatBitwiseTerm[CVC4::Expr& f]
std::vector<unsigned> operators;
unsigned op;
}
- : bitwiseXorTerm[f] { expressions.push_back(f); }
- ( concatBitwiseBinop[op] bitwiseXorTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
+ : bvNegTerm[f] { expressions.push_back(f); }
+ ( concatBitwiseBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )*
{ f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); }
;
concatBitwiseBinop[unsigned& op]
@@ -1072,7 +1081,56 @@ concatBitwiseBinop[unsigned& op]
| BVAND_TOK
;
-bitwiseXorTerm[CVC4::Expr& f]
+bvNegTerm[CVC4::Expr& f]
+ /* BV neg */
+ : BVNEG_TOK bvNegTerm[f]
+ { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
+ | selectExtractShift[f]
+ ;
+
+/**
+ * Parses an array select / bitvector extract / bitvector shift.
+ * These are all parsed the same way because they are all effectively
+ * post-fix operators and can continue piling onto an expression.
+ * Array selects and bitvector extracts even share similar syntax with
+ * their use of [ square brackets ], so we left-factor as much out as
+ * possible to make ANTLR happy.
+ */
+selectExtractShift[CVC4::Expr& f]
+@init {
+ Expr f2;
+ bool extract, left;
+}
+ : bvTerm[f]
+ ( /* array select / bitvector extract */
+ LBRACKET
+ ( formula[f2] { extract = false; }
+ | k1=numeral COLON k2=numeral { extract = true; } )
+ RBRACKET
+ { if(extract) {
+ /* bitvector extract */
+ f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
+ } else {
+ /* array select */
+ f = MK_EXPR(CVC4::kind::SELECT, f, f2);
+ }
+ }
+ | ( LEFTSHIFT_TOK { left = true; }
+ | RIGHTSHIFT_TOK { left = false; } ) k=numeral
+ { // Defined in:
+ // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
+ if(left) {
+ f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
+ } else {
+ unsigned n = BitVectorType(f.getType()).getSize();
+ f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
+ MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
+ }
+ }
+ )*
+ ;
+
+bvTerm[CVC4::Expr& f]
@init {
Expr f2;
}
@@ -1087,27 +1145,15 @@ bitwiseXorTerm[CVC4::Expr& f]
{ f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); }
| BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); }
- | bvNegTerm[f]
- ;
-bvNegTerm[CVC4::Expr& f]
- /* BV neg */
- : BVNEG_TOK bvNegTerm[f]
- { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
- | bvUminusTerm[f]
- ;
-bvUminusTerm[CVC4::Expr& f]
-@init {
- Expr f2;
-}
+
/* BV unary minus */
- : BVUMINUS_TOK LPAREN formula[f] RPAREN
+ | BVUMINUS_TOK LPAREN formula[f] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); }
/* BV addition */
| BVPLUS_TOK LPAREN k=numeral COMMA formula[f]
( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN
{ unsigned size = BitVectorType(f.getType()).getSize();
if(k == 0) {
-# warning cannot do BVPLUS(...)[i:j]
PARSER_STATE->parseError("BVPLUS(k,_,_,...) must have k > 0");
}
if(k > size) {
@@ -1191,35 +1237,9 @@ bvUminusTerm[CVC4::Expr& f]
/* BV rotate left */
| BVROTL_TOK LPAREN formula[f] COMMA k=numeral RPAREN
{ f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); }
- /* left and right shifting with << and >>, or something else */
- | bvShiftTerm[f]
- ;
-bvShiftTerm[CVC4::Expr& f]
-@init {
- bool left = false;
-}
- : bvComparison[f]
- ( (LEFTSHIFT_TOK { left = true; } | RIGHTSHIFT_TOK) k=numeral
- { // Defined in:
- // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
- if(left) {
- f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
- } else {
- unsigned n = BitVectorType(f.getType()).getSize();
- f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)),
- MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f));
- }
- }
- )?
- ;
-
-bvComparison[CVC4::Expr& f]
-@init {
- Expr f2;
-}
/* BV comparisons */
- : BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
+ | BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); }
| BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); }
@@ -1235,35 +1255,13 @@ bvComparison[CVC4::Expr& f]
{ f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); }
| BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); }
+
/*
| IS_INTEGER_TOK LPAREN formula[f] RPAREN
{ f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); }
*/
- | selectExtractTerm[f]
- ;
-
-/** Parses an array select. */
-selectExtractTerm[CVC4::Expr& f]
-@init {
- Expr f2;
- bool extract;
-}
- /* array select / bitvector extract */
- : simpleTerm[f]
- ( { extract = false; }
- LBRACKET formula[f2] ( COLON k2=numeral { extract = true; } )? RBRACKET
- { if(extract) {
- if(f2.getKind() != kind::CONST_INTEGER) {
- PARSER_STATE->parseError("bitvector extraction requires [numeral:numeral] range");
- }
- unsigned k1 = f2.getConst<Integer>().getLong();
- f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f);
- } else {
- f = MK_EXPR(CVC4::kind::SELECT, f, f2);
- }
- }
- )*
+ | simpleTerm[f]
;
/** Parses a simple term. */
@@ -1447,13 +1445,7 @@ selector[CVC4::Datatype::Constructor& ctor]
Type t;
}
: identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE]
- { if(t.isNull()) {
-# warning FIXME datatypes
- //std::pair<Type, std::string> unresolved = PARSER_STATE->newUnresolvedType();
- //ctor.addArg(id, Datatype::UnresolvedType(unresolved.second);
- } else {
- ctor.addArg(id, t);
- }
+ { ctor.addArg(id, t);
Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
}
;
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index 9a5b654a8..d32914d8e 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -5,7 +5,7 @@
** Major contributors: cconway
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -64,14 +64,12 @@ public:
// Destructor
virtual ~ParserException() throw() {}
- virtual std::string toString() const {
+ virtual void toStream(std::ostream& os) const {
if( d_line > 0 ) {
- std::stringstream ss;
- ss << "Parse Error: " << d_filename << ":" << d_line << "."
+ os << "Parse Error: " << d_filename << ":" << d_line << "."
<< d_column << ": " << d_msg;
- return ss.str();
} else {
- return "Parse Error: " + d_msg;
+ os << "Parse Error: " << d_msg;
}
}
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 409518fcf..e23d7c88b 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -182,7 +182,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
out << "BVROTR(" << n[0] << "," << n.getOperator() << ')';
break;
-
default:
out << n.getOperator();
if(n.getNumChildren() > 0) {
@@ -233,15 +232,20 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2];
break;
- // these are prefix
+ // these are prefix and have an extra size 'k' as first argument
case kind::BITVECTOR_PLUS:
case kind::BITVECTOR_SUB:
+ case kind::BITVECTOR_MULT:
+ out << n.getOperator() << '(' << n.getType().getBitVectorSize() << ','
+ << n[0] << ',' << n[1] << ')';
+ break;
+
+ // these are prefix
case kind::BITVECTOR_XOR:
case kind::BITVECTOR_NAND:
case kind::BITVECTOR_NOR:
case kind::BITVECTOR_XNOR:
case kind::BITVECTOR_COMP:
- case kind::BITVECTOR_MULT:
case kind::BITVECTOR_UDIV:
case kind::BITVECTOR_UREM:
case kind::BITVECTOR_SDIV:
@@ -267,7 +271,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
out << n[0][0] << " /= " << n[0][1];
} else if(n.getNumChildren() == 2) {
// infix operator
- out << n[0] << ' ' << n.getOperator() << ' ' << n[1];
+ out << '(' << n[0] << ' ' << n.getOperator() << ' ' << n[1] << ')';
+ } else if(k == kind::BITVECTOR_NOT) {
+ // precedence on ~ is a little unexpected; add parens
+ out << "(~(" << n[0] << "))";
} else {
// prefix operator
out << n.getOperator() << ' ';
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2467db3bb..376a8a531 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3,7 +3,7 @@
** \verbatim
** Original author: mdeters
** Major contributors: dejan
- ** Minor contributors (to current version): taking, cconway
+ ** Minor contributors (to current version): cconway
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
@@ -346,7 +346,8 @@ void SmtEngine::defineFunction(Expr func,
FunctionType(funcType).getRangeType() : funcType;
if(formulaType != rangeType) {
stringstream ss;
- ss << "Defined function's declared type does not match that of body\n"
+ ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+ << "Defined function's declared type does not match that of body\n"
<< "The function : " << func << "\n"
<< "Its range type: " << rangeType << "\n"
<< "The body : " << formula << "\n"
@@ -474,9 +475,11 @@ Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode in)
// theory could still create a new expression that isn't
// well-typed, and we don't want the C++ runtime to abort our
// process without any error notice.
- InternalError("A bad expression was produced. "
- "Original exception follows:\n%s",
- tcep.toString().c_str());
+ stringstream ss;
+ ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+ << "A bad expression was produced. Original exception follows:\n"
+ << tcep;
+ InternalError(ss.str().c_str());
}
}
@@ -503,9 +506,11 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
// theory could still create a new expression that isn't
// well-typed, and we don't want the C++ runtime to abort our
// process without any error notice.
- InternalError("A bad expression was produced. "
- "Original exception follows:\n%s",
- tcep.toString().c_str());
+ stringstream ss;
+ ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+ << "A bad expression was produced. Original exception follows:\n"
+ << tcep;
+ InternalError(ss.str().c_str());
}
}
@@ -514,7 +519,8 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) {
Type boolType = d_exprManager->booleanType();
if(type != boolType) {
stringstream ss;
- ss << "Expected " << boolType << "\n"
+ ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage))
+ << "Expected " << boolType << "\n"
<< "The assertion : " << e << "\n"
<< "Its type : " << type;
throw TypeCheckingException(e, ss.str());
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 9f24e9873..11e8a8443 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -5,7 +5,7 @@
** Major contributors: cconway
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -31,6 +31,9 @@ struct ArraySelectTypeRule {
Assert(n.getKind() == kind::SELECT);
TypeNode arrayType = n[0].getType(check);
if( check ) {
+ if(!arrayType.isArray()) {
+ throw TypeCheckingExceptionPrivate(n, "array select operating on non-array");
+ }
TypeNode indexType = n[1].getType(check);
if(arrayType.getArrayIndexType() != indexType) {
throw TypeCheckingExceptionPrivate(n, "array select not indexed with correct type for array");
@@ -46,6 +49,9 @@ struct ArrayStoreTypeRule {
Assert(n.getKind() == kind::STORE);
TypeNode arrayType = n[0].getType(check);
if( check ) {
+ if(!arrayType.isArray()) {
+ throw TypeCheckingExceptionPrivate(n, "array store operating on non-array");
+ }
TypeNode indexType = n[1].getType(check);
TypeNode valueType = n[2].getType(check);
if(arrayType.getArrayIndexType() != indexType) {
diff --git a/src/util/exception.h b/src/util/exception.h
index 4893bd3c2..1b1eb224e 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -21,7 +21,9 @@
#ifndef __CVC4__EXCEPTION_H
#define __CVC4__EXCEPTION_H
+#include <iostream>
#include <string>
+#include <sstream>
namespace CVC4 {
@@ -38,16 +40,36 @@ public:
// NON-VIRTUAL METHOD for setting and printing the error message
void setMessage(const std::string& msg) { d_msg = msg; }
std::string getMessage() const { return d_msg; }
- // Printing: feel free to redefine toString(). When inherited,
- // it's recommended that this method print the type of exception
- // before the actual message.
- virtual std::string toString() const { return d_msg; }
+ /**
+ * Get this exception as a string. Note that
+ * cout << ex.toString();
+ * is subtly different from
+ * cout << ex;
+ * which is equivalent to
+ * ex.toStream(cout);
+ * That is because with the latter two, the output language (and
+ * other preferences) for exprs on the stream is respected. In
+ * toString(), there is no stream, so the parameters are default
+ * and you'll get exprs and types printed using the AST language.
+ */
+ std::string toString() const {
+ std::stringstream ss;
+ toStream(ss);
+ return ss.str();
+ }
+ /**
+ * Printing: feel free to redefine toStream(). When overridden in
+ * a derived class, it's recommended that this method print the
+ * type of exception before the actual message.
+ */
+ virtual void toStream(std::ostream& os) const { os << d_msg; }
// No need to overload operator<< for the inherited classes
friend std::ostream& operator<<(std::ostream& os, const Exception& e);
};/* class Exception */
inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
- return os << e.toString();
+ e.toStream(os);
+ return os;
}
}/* CVC4 namespace */
diff --git a/src/util/language.h b/src/util/language.h
index fdd2a382d..814f8dcd1 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -5,7 +5,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -138,12 +138,29 @@ typedef language::output::Language OutputLanguage;
namespace language {
+inline InputLanguage toInputLanguage(OutputLanguage language) {
+ switch(language) {
+ case output::LANG_SMTLIB:
+ case output::LANG_SMTLIB_V2:
+ case output::LANG_CVC4:
+ // these entries directly correspond (by design)
+ return InputLanguage(int(language));
+
+ default: {
+ std::stringstream ss;
+ ss << "Cannot map output language `" << language
+ << "' to an input language.";
+ throw CVC4::Exception(ss.str());
+ }
+ }/* switch(language) */
+}/* toInputLanguage() */
+
inline OutputLanguage toOutputLanguage(InputLanguage language) {
switch(language) {
case input::LANG_SMTLIB:
case input::LANG_SMTLIB_V2:
case input::LANG_CVC4:
- // these entries correspond
+ // these entries directly correspond (by design)
return OutputLanguage(int(language));
default: {
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index edda090ba..493572dc9 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -23,4 +23,4 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
EXTRA_DIST = $(TESTS) \
test00.smt \
- bvcomp.smt
+ bvcomp.cvc
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index 821b43a2f..abce24751 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -13,11 +13,17 @@
**
** \brief "Ouroborous" test: does CVC4 read its own output?
**
- ** The "Ouroborous" test, named after the serpent that swallows its own
- ** tail, ensures that CVC4 can parse some input, output it again (in any
- ** of its languages) and then parse it again. The result of the first
- ** parse must be equal to the result of the second parse (up to renaming
- ** variables), or the test fails.
+ ** The "Ouroborous" test, named after the serpent that swallows its
+ ** own tail, ensures that CVC4 can parse some input, output it again
+ ** (in any of its languages) and then parse it again. The result of
+ ** the first parse must be equal to the result of the second parse;
+ ** both strings and expressions are compared for equality.
+ **
+ ** To add a new test, simply add a call to runTestString() under
+ ** runTest(), below. If you don't specify an input language,
+ ** LANG_SMTLIB_V2 is used. If your example depends on variables,
+ ** you'll need to declare them in the "declarations" global, just
+ ** below, in SMT-LIBv2 form (but they're good for all languages).
**/
#include <iostream>
@@ -40,8 +46,11 @@ const string declarations = "\
(declare-fun x () U)\n\
(declare-fun y () U)\n\
(assert (= (f x) x))\n\
+(declare-fun a () (Array U (Array U U)))\n\
";
+Parser* psr = NULL;
+
int runTest();
int main() {
@@ -55,25 +64,52 @@ int main() {
return 1;
}
-string translate(Parser* parser, string in, InputLanguage inlang, OutputLanguage outlang) {
+string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
cout << "==============================================" << endl
<< "translating from " << inlang << " to " << outlang << " this string:" << endl
<< in << endl;
- parser->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
+ psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
+ Expr e = psr->nextExpression();
stringstream ss;
- ss << Expr::setlanguage(outlang) << parser->nextExpression();
- AlwaysAssert(parser->nextExpression().isNull(), "next expr should be null");
- AlwaysAssert(parser->done(), "parser should be done");
+ ss << Expr::setlanguage(outlang) << Expr::setdepth(-1) << e;
+ AlwaysAssert(psr->nextExpression().isNull(), "next expr should be null");
+ AlwaysAssert(psr->done(), "parser should be done");
string s = ss.str();
cout << "got this:" << endl
<< s << endl
+ << "reparsing as " << outlang << endl;
+
+ psr->setInput(Input::newStringInput(toInputLanguage(outlang), s, "internal-buffer"));
+ Expr f = psr->nextExpression();
+ AlwaysAssert(e == f);
+ cout << "got same expressions " << e.getId() << " and " << f.getId() << endl
<< "==============================================" << endl;
+
return s;
}
+void runTestString(std::string instr, InputLanguage instrlang = input::LANG_SMTLIB_V2) {
+ cout << endl
+ << "starting with: " << instr << endl
+ << " in language " << instrlang << endl;
+ string smt2 = translate(instr, instrlang, output::LANG_SMTLIB_V2);
+ cout << "in SMT2 : " << smt2 << endl;
+ /* -- SMT-LIBv1 doesn't have a functional printer yet
+ string smt1 = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
+ cout << "in SMT1 : " << smt1 << endl;
+ */
+ string cvc = translate(smt2, input::LANG_SMTLIB_V2, output::LANG_CVC4);
+ cout << "in CVC : " << cvc << endl;
+ string out = translate(cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
+ cout << "back to SMT2 : " << out << endl << endl;
+
+ AlwaysAssert(out == smt2, "differences in output");
+}
+
+
int runTest() {
ExprManager em;
- Parser* parser =
+ psr =
ParserBuilder(&em, "internal-buffer")
.withStringInput(declarations)
.withInputLanguage(input::LANG_SMTLIB_V2)
@@ -81,27 +117,20 @@ int runTest() {
// we don't need to execute them, but we DO need to parse them to
// get the declarations
- while(Command* c = parser->nextCommand()) {
+ while(Command* c = psr->nextCommand()) {
delete c;
}
- AlwaysAssert(parser->done(), "parser should be done");
+ AlwaysAssert(psr->done(), "parser should be done");
- string instr = "(= (f (f y)) x)";
- cout << "starting with: " << instr << endl;
- string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2);
- cout << "in SMT2 : " << smt2 << endl;
- string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
- cout << "in SMT1 : " << smt1 << endl;
- string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4);
- cout << "in CVC : " << cvc << endl;
- string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
- cout << "back to SMT2 : " << out << endl;
+ cout << Expr::setdepth(-1);
- AlwaysAssert(out == smt2, "differences in output");
+ runTestString("(= (f (f y)) x)");
+ runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4);
+ runTestString("a[x][y] = a[y][x]", input::LANG_CVC4);
- delete parser;
+ delete psr;
+ psr = NULL;
return 0;
}
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback