From: Morgan Deters Date: Wed, 20 Apr 2011 07:57:28 +0000 (+0000) Subject: Minor mixed-bag commit. Expected performance impact negligible. X-Git-Tag: cvc5-1.0.0~8585 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce04216289985021ce53588e3040e2ac9d6a2a0d;p=cvc5.git Minor mixed-bag commit. Expected performance impact negligible. * Fixed hole in arrays typechecking. * Fixed "make dist". * Better ouroborous test, and some printer fixes. * Continued cleanup in CVC parser, removed some warnings. * Better output. --- 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 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 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 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 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().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 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 #include +#include 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 @@ -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; } -