From e761169680c7611f5429f11bf5050370036dcff5 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Sun, 5 Feb 2012 21:44:02 +0000 Subject: [PATCH] changes to the cvc4 language printer, so that it actually prints the cvc4 language all theory writers should take a look a what's being printed, to ensure all cases are covered --- src/printer/cvc/cvc_printer.cpp | 502 +++++++++++++++++++++----------- src/printer/cvc/cvc_printer.h | 5 +- 2 files changed, 333 insertions(+), 174 deletions(-) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8d76a7332..1bcb4892b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -36,15 +36,21 @@ namespace CVC4 { namespace printer { namespace cvc { -void CvcPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const throw() { +void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, bool bracket) const throw() +{ + if (depth == 0) { + out << "(...)"; + } else { + depth --; + } + // null if(n.getKind() == kind::NULL_EXPR) { out << "NULL"; return; } - // variable + // variables if(n.getMetaKind() == kind::metakind::VARIABLE) { string s; if(n.getAttribute(expr::VarNameAttr(), s)) { @@ -62,11 +68,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << ":"; n.getType().toStream(out, -1, false, language::output::LANG_CVC4); } - return; } - // constant + // constants if(n.getMetaKind() == kind::metakind::CONSTANT) { switch(n.getKind()) { case kind::BITVECTOR_TYPE: @@ -92,6 +97,16 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')'; break; } + case kind::CONST_INTEGER: { + const Integer& num = n.getConst(); + out << num; + break; + } + case kind::CONST_PSEUDOBOOLEAN: { + const Pseudoboolean& num = n.getConst(); + out << num; + break; + } case kind::TYPE_CONSTANT: switch(TypeConstant tc = n.getConst()) { case REAL_TYPE: @@ -111,136 +126,154 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, break; default: out << tc; - } - break; - case kind::BUILTIN: - switch(Kind k = n.getConst()) { - case kind::EQUAL: out << '='; break; - case kind::PLUS: out << '+'; break; - case kind::MULT: out << '*'; break; - case kind::MINUS: - case kind::UMINUS: out << '-'; break; - case kind::DIVISION: out << '/'; break; - case kind::LT: out << '<'; break; - case kind::LEQ: out << "<="; break; - case kind::GT: out << '>'; break; - case kind::GEQ: out << ">="; break; - case kind::IMPLIES: out << "=>"; break; - case kind::IFF: out << "<=>"; break; - - // names are slightly different than the kind - case kind::BITVECTOR_PLUS: out << "BVPLUS"; break; - case kind::BITVECTOR_SUB: out << "BVSUB"; break; - case kind::BITVECTOR_XOR: out << "BVXOR"; break; - case kind::BITVECTOR_NAND: out << "BVNAND"; break; - case kind::BITVECTOR_NOR: out << "BVNOR"; break; - case kind::BITVECTOR_XNOR: out << "BVXNOR"; break; - case kind::BITVECTOR_COMP: out << "BVCOMP"; break; - case kind::BITVECTOR_MULT: out << "BVMULT"; break; - case kind::BITVECTOR_UDIV: out << "BVUDIV"; break; - case kind::BITVECTOR_UREM: out << "BVUREM"; break; - case kind::BITVECTOR_SDIV: out << "BVSDIV"; break; - case kind::BITVECTOR_SREM: out << "BVSREM"; break; - case kind::BITVECTOR_SMOD: out << "BVSMOD"; break; - case kind::BITVECTOR_SHL: out << "BVSHL"; break; - case kind::BITVECTOR_LSHR: out << "BVLSHR"; break; - case kind::BITVECTOR_ASHR: out << "BVASHR"; break; - case kind::BITVECTOR_ULT: out << "BVLT"; break; - case kind::BITVECTOR_ULE: out << "BVLE"; break; - case kind::BITVECTOR_UGT: out << "BVGT"; break; - case kind::BITVECTOR_UGE: out << "BVGE"; break; - case kind::BITVECTOR_SLT: out << "BVSLT"; break; - case kind::BITVECTOR_SLE: out << "BVSLE"; break; - case kind::BITVECTOR_SGT: out << "BVSGT"; break; - case kind::BITVECTOR_SGE: out << "BVSGE"; break; - case kind::BITVECTOR_NEG: out << "BVUMINUS"; break; - - case kind::BITVECTOR_NOT: out << "~"; break; - case kind::BITVECTOR_AND: out << "&"; break; - case kind::BITVECTOR_OR: out << "|"; break; - case kind::BITVECTOR_CONCAT: out << "@"; break; - - default: - out << k; + break; } break; default: - // fall back on whatever operator<< does on underlying type; we - // might luck out and be SMT-LIB v2 compliant - kind::metakind::NodeValueConstPrinter::toStream(out, n); + Unreachable(); + break; } - return; - } else if(n.getMetaKind() == kind::metakind::PARAMETERIZED) { - switch(n.getKind()) { - case kind::SORT_TYPE: { - std::string name; - if(n.getAttribute(expr::VarNameAttr(), name)) { - out << name; - } else { - goto default_case; + } + + enum OpType { + PREFIX, + INFIX, + POSTFIX + } opType; + + stringstream op; // operation (such as '+') + + switch(n.getKind()) { + + // BUILTIN + case kind::EQUAL: + op << '='; + opType = INFIX; + break; + case kind::ITE: + out << "IF "; + toStream(out, n[0], depth, types, true); + out << " THEN "; + toStream(out, n[1], depth, types, true); + out << " ELSE "; + toStream(out, n[2], depth, types, true); + return; + break; + case kind::TUPLE_TYPE: + out << '['; + for (unsigned i = 0; i < n.getNumChildren(); ++ i) { + if (i > 0) { + out << ", "; + } + toStream(out, n[i], depth, types, false); } + out << ']'; + return; break; - } - case kind::BITVECTOR_EXTRACT: - out << n[0] << n.getOperator().getConst(); + case kind::TUPLE: + // no-op break; - case kind::BITVECTOR_REPEAT: - out << "BVREPEAT(" << n[0] << "," << n.getOperator() << ')'; + case kind::APPLY: + toStream(op, n.getOperator(), depth, types, true); break; - case kind::BITVECTOR_ZERO_EXTEND: - out << "BVZEROEXTEND(" << n[0] << "," << n.getOperator() << ')'; + + // BOOL + case kind::AND: + op << "AND"; + opType = INFIX; break; - case kind::BITVECTOR_SIGN_EXTEND: - out << "SX(" << n[0] << "," << n.getOperator() << ')'; + case kind::OR: + op << "OR"; + opType = INFIX; break; - case kind::BITVECTOR_ROTATE_LEFT: - out << "BVROTL(" << n[0] << "," << n.getOperator() << ')'; + case kind::NOT: + op << "NOT"; + opType = PREFIX; break; - case kind::BITVECTOR_ROTATE_RIGHT: - out << "BVROTR(" << n[0] << "," << n.getOperator() << ')'; + case kind::XOR: + op << "XOR"; + opType = INFIX; + break; + case kind::IFF: + op << "<=>"; + opType = INFIX; + break; + case kind::IMPLIES: + op << "=>"; + opType = INFIX; break; - default: - default_case: - out << n.getOperator(); - if(n.getNumChildren() > 0) { - out << '('; - if(n.getNumChildren() > 1) { - copy(n.begin(), n.end() - 1, ostream_iterator(out, ", ")); + // UF + case kind::APPLY_UF: + toStream(op, n.getOperator(), depth, types, true); + break; + case kind::FUNCTION_TYPE: + if (n.getNumChildren() > 1) { + if (n.getNumChildren() > 2) { + out << '('; + } + for (unsigned i = 0; i < n.getNumChildren(); ++ i) { + if (i > 0) { + out << ", "; + } + toStream(out, n[i], depth, types, false); + } + if (n.getNumChildren() > 2) { + out << ')'; } - out << n[n.getNumChildren() - 1] << ')'; } - } - return; - } else if(n.getMetaKind() == kind::metakind::OPERATOR) { - switch(Kind k = n.getKind()) { - case kind::FUNCTION_TYPE: + out << " -> "; + toStream(out, n[n.getNumChildren()-1], depth, types, false); + return; + break; + + // DATATYPES + case kind::APPLY_CONSTRUCTOR: + case kind::APPLY_SELECTOR: + case kind::APPLY_TESTER: + toStream(op, n.getOperator(), depth, types, false); + break; case kind::CONSTRUCTOR_TYPE: case kind::SELECTOR_TYPE: - if(n.getNumChildren() > 2) { - out << '('; - for(unsigned i = 0; i < n.getNumChildren() - 2; ++i) { - out << n[i] << ", "; + if (n.getNumChildren() > 1) { + if (n.getNumChildren() > 2) { + out << '('; + } + for (unsigned i = 0; i < n.getNumChildren(); ++ i) { + if (i > 0) { + out << ", "; + } + toStream(out, n[i], depth, types, false); + } + if (n.getNumChildren() > 2) { + out << ')'; } - out << n[n.getNumChildren() - 2] - << ") -> " << n[n.getNumChildren() - 1]; - } else if(n.getNumChildren() == 2) { - out << n[0] << " -> " << n[1]; - } else { - Assert(n.getNumChildren() == 1); - out << n[0]; } + out << " -> "; + toStream(out, n[n.getNumChildren()-1], depth, types, false); + return; break; case kind::TESTER_TYPE: - out << n[0] << " -> BOOLEAN"; + toStream(out, n[0], depth, types, false); + out << " -> BOOLEAN"; + return; break; + // ARRAYS case kind::ARRAY_TYPE: - out << "ARRAY " << n[0] << " OF " << n[1]; + out << "ARRAY "; + toStream(out, n[0], depth, types, false); + out << " OF "; + toStream(out, n[1], depth, types, false); + return; break; case kind::SELECT: - out << n[0] << '[' << n[1] << ']'; + toStream(out, n[0], depth, types, false); + out << '['; + toStream(out, n[0], depth, types, false); + out << ']'; + return; break; case kind::STORE: { stack stk; @@ -248,117 +281,240 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, while(stk.top()[0].getKind() == kind::STORE) { stk.push(stk.top()[0]); } - out << '('; + if (bracket) { + out << '('; + } TNode x = stk.top(); - out << x[0] << " WITH [" << x[1] << "] := " << x[2]; + toStream(out, x[0], depth, types, false); + out << " WITH ["; + toStream(out, x[1], depth, types, false); + out << "] := "; + toStream(out, x[2], depth, types, false); stk.pop(); while(!stk.empty()) { x = stk.top(); - out << ", [" << x[1] << "] := " << x[2]; + out << ", ["; + toStream(out, x[1], depth, types, false); + out << "] := "; + toStream(out, x[2], depth, types, false); stk.pop(); } - out << ')'; + if (bracket) { + out << ')'; + } + return; break; } - case kind::TUPLE_TYPE: - out << '['; - copy(n.begin(), n.end() - 1, ostream_iterator(out, ",")); - out << n[n.getNumChildren() - 1]; - out << ']'; + // ARITHMETIC + case kind::PLUS: + op << '+'; + opType = INFIX; break; - case kind::TUPLE: - out << "( "; - copy(n.begin(), n.end() - 1, ostream_iterator(out, ", ")); - out << n[n.getNumChildren() - 1]; - out << " )"; + case kind::MULT: + op << '*'; + opType = INFIX; break; - - case kind::ITE: - out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2]; + case kind::MINUS: + op << '-'; + opType = INFIX; + break; + case kind::UMINUS: + op << '-'; + opType = PREFIX; + break; + case kind::DIVISION: + op << '/'; + opType = INFIX; + break; + case kind::LT: + op << '<'; + opType = INFIX; + break; + case kind::LEQ: + op << "<="; + opType = INFIX; + break; + case kind::GT: + op << '>'; + opType = INFIX; + break; + case kind::GEQ: + op << ">="; + opType = INFIX; break; - // these are prefix and have an extra size 'k' as first argument + // BITVECTORS case kind::BITVECTOR_PLUS: + op << "BVPLUS"; + break; case kind::BITVECTOR_SUB: - case kind::BITVECTOR_MULT: - out << n.getOperator() << '(' << n.getType().getBitVectorSize() << ',' - << n[0] << ',' << n[1] << ')'; + op << "BVSUB"; break; - - // these are prefix case kind::BITVECTOR_XOR: + op << "BVXOR"; + break; case kind::BITVECTOR_NAND: + op << "BVNAND"; + break; case kind::BITVECTOR_NOR: + op << "BVNOR"; + break; case kind::BITVECTOR_XNOR: + op << "BVXNOR"; + break; case kind::BITVECTOR_COMP: + op << "BVCOMP"; + break; + case kind::BITVECTOR_MULT: + op << "BVMULT"; + break; case kind::BITVECTOR_UDIV: + op << "BVUDIV"; + break; case kind::BITVECTOR_UREM: + op << "BVUREM"; + break; case kind::BITVECTOR_SDIV: + op << "BVSDIV"; + break; case kind::BITVECTOR_SREM: + op << "BVSREM"; + break; case kind::BITVECTOR_SMOD: + op << "BVSMOD"; + break; case kind::BITVECTOR_SHL: + op << "BVSHL"; + break; case kind::BITVECTOR_LSHR: + op << "BVLSHR"; + break; case kind::BITVECTOR_ASHR: + op << "BVASHR"; + break; case kind::BITVECTOR_ULT: + op << "BVLT"; + break; case kind::BITVECTOR_ULE: + op << "BVLE"; + break; case kind::BITVECTOR_UGT: + op << "BVGT"; + break; case kind::BITVECTOR_UGE: + op << "BVGE"; + break; case kind::BITVECTOR_SLT: + op << "BVSLT"; + break; case kind::BITVECTOR_SLE: + op << "BVSLE"; + break; case kind::BITVECTOR_SGT: + op << "BVSGT"; + break; case kind::BITVECTOR_SGE: - out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')'; + op << "BVSGE"; + break; + case kind::BITVECTOR_NEG: + op << "BVUMINUS"; + break; + case kind::BITVECTOR_NOT: + op << "~"; + break; + case kind::BITVECTOR_AND: + op << "&"; + opType = INFIX; + break; + case kind::BITVECTOR_OR: + op << "|"; + opType = INFIX; break; - - // N-ary infix case kind::BITVECTOR_CONCAT: + op << "@"; + opType = INFIX; + break; + case kind::BITVECTOR_EXTRACT: + op << n.getOperator().getConst(); + opType = POSTFIX; + break; + case kind::BITVECTOR_REPEAT: + out << "BVREPEAT("; + toStream(out, n[0], depth, types, false); + out << ", " << n.getOperator().getConst() << ')'; + return; + break; + case kind::BITVECTOR_ZERO_EXTEND: + out << "BVZEROEXTEND("; + toStream(out, n[0], depth, types, false); + out << ", " << n.getOperator().getConst() << ')'; + return; + break; + case kind::BITVECTOR_SIGN_EXTEND: + out << "SX("; + toStream(out, n[0], depth, types, false); + out << ", " << n.getOperator().getConst() << ')'; + return; + break; + case kind::BITVECTOR_ROTATE_LEFT: + out << "BVROTL("; + toStream(out, n[0], depth, types, false); + out << ", " << n.getOperator().getConst() << ')'; + return; + break; + case kind::BITVECTOR_ROTATE_RIGHT: + out << "BVROTR("; + toStream(out, n[0], depth, types, false); + out << ", " << n.getOperator().getConst() << ')'; + return; + break; + default: + Unreachable(); + break; + } + + switch (opType) { + case PREFIX: + if (bracket) { + out << op.str() << '('; + } + break; + case INFIX: + if (bracket) { out << '('; - for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { - out << n[i] << ' ' << n.getOperator(); - } - out << n[n.getNumChildren() - 1] << ')'; + } + break; + case POSTFIX: + break; + } - default: - if(k == kind::NOT && n[0].getKind() == kind::EQUAL) { - // collapse NOT-over-EQUAL - out << n[0][0] << " /= " << n[0][1]; - } else if(n.getNumChildren() == 2) { - // infix binary operator - out << '(' << n[0] << ' ' << n.getOperator() << ' ' << n[1] << ')'; - } else if(n.getKind() == kind::AND || - n.getKind() == kind::OR || - n.getKind() == kind::PLUS || - n.getKind() == kind::MULT) { - // infix N-ary operator - TNode::iterator i = n.begin(); - out << '(' << *i++; - while(i != n.end()) { - out << ' ' << n.getOperator() << ' ' << *i++; - } - out << ')'; - } else if(k == kind::BITVECTOR_NOT) { - // precedence on ~ is a little unexpected; add parens - out << "(~(" << n[0] << "))"; + for (unsigned i = 0; i < n.getNumChildren(); ++ i) { + if (i > 0) { + if (opType == INFIX) { + out << ' ' << op.str() << ' '; } else { - // prefix N-ary operator for N != 2 - if(n.getNumChildren() == 0) { - // no parens or spaces - out << n.getOperator(); - } else { - out << '(' << n.getOperator() << ' '; - if(n.getNumChildren() > 1) { - copy(n.begin(), n.end() - 1, ostream_iterator(out, " ")); - } - out << n[n.getNumChildren() - 1] << ')'; - } + out << ", "; } } - return; + toStream(out, n[i], depth, types, opType == INFIX); } - // shouldn't ever happen (unless new metakinds are added) - Unhandled(); + switch (opType) { + case PREFIX: + if (bracket) { + out << ')'; + } + break; + case INFIX: + if (bracket) { + out << ')'; + } + break; + case POSTFIX: + out << op.str(); + break; + } }/* CvcPrinter::toStream(TNode) */ diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index ba66145fc..3db3f2c66 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -30,8 +30,11 @@ namespace printer { namespace cvc { class CvcPrinter : public CVC4::Printer { + void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw(); public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw() { + toStream(out, n, toDepth, types, false); + } void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class CvcPrinter */ -- 2.30.2