From 57b54a2eba7904652dfaf7e32b4eac8abd22c79b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Dec 2020 10:17:09 -0600 Subject: Use new let binding for cvc printer (#5561) Also changes names slightly to avoid accidental uses of toStream, which can lead to infinite loops if the wrong version is used. --- src/printer/cvc/cvc_printer.cpp | 211 ++++++++++++++++++++++------------------ 1 file changed, 117 insertions(+), 94 deletions(-) (limited to 'src/printer/cvc/cvc_printer.cpp') diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index be530099b..c681a223f 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -31,7 +31,7 @@ #include "expr/sequence.h" #include "options/language.h" // for LANG_AST #include "options/smt_options.h" -#include "printer/dagification_visitor.h" +#include "printer/let_binding.h" #include "smt/command.h" #include "smt/node_command.h" #include "smt/smt_engine.h" @@ -51,31 +51,10 @@ void CvcPrinter::toStream(std::ostream& out, size_t dag) const { if(dag != 0) { - DagificationVisitor dv(dag); - NodeVisitor visitor; - visitor.run(dv, n); - const theory::SubstitutionMap& lets = dv.getLets(); - if(!lets.empty()) { - out << "LET "; - bool first = true; - for(theory::SubstitutionMap::const_iterator i = lets.begin(); - i != lets.end(); - ++i) { - if(! first) { - out << ", "; - } else { - first = false; - } - toStream(out, (*i).second, toDepth, false); - out << " = "; - toStream(out, (*i).first, toDepth, false); - } - out << " IN "; - } - Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth, false); + LetBinding lbind(dag + 1); + toStreamNodeWithLetify(out, n, toDepth, false, &lbind); } else { - toStream(out, n, toDepth, false); + toStreamNode(out, n, toDepth, false, nullptr); } } @@ -93,10 +72,11 @@ void toStreamRational(std::ostream& out, Node n, bool forceRational) } } -void CvcPrinter::toStream(std::ostream& out, - TNode n, - int depth, - bool bracket) const +void CvcPrinter::toStreamNode(std::ostream& out, + TNode n, + int depth, + bool bracket, + LetBinding* lbind) const { if (depth == 0) { out << "(...)"; @@ -286,11 +266,11 @@ void CvcPrinter::toStream(std::ostream& out, break; case kind::ITE: out << "IF "; - toStream(out, n[0], depth, true); + toStreamNode(out, n[0], depth, true, lbind); out << " THEN "; - toStream(out, n[1], depth, true); + toStreamNode(out, n[1], depth, true, lbind); out << " ELSE "; - toStream(out, n[2], depth, true); + toStreamNode(out, n[2], depth, true, lbind); out << " ENDIF"; return; break; @@ -300,7 +280,7 @@ void CvcPrinter::toStream(std::ostream& out, if (i > 0) { out << ", "; } - toStream(out, n[i], depth, false); + toStreamNode(out, n[i], depth, false, lbind); } out << ']'; return; @@ -310,22 +290,22 @@ void CvcPrinter::toStream(std::ostream& out, break; case kind::LAMBDA: out << "(LAMBDA"; - toStream(out, n[0], depth, true); + toStreamNode(out, n[0], depth, true, lbind); out << ": "; - toStream(out, n[1], depth, true); + toStreamNodeWithLetify(out, n[1], depth, true, lbind); out << ")"; return; break; case kind::WITNESS: out << "(WITNESS"; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, true, lbind); out << " : "; - toStream(out, n[1], depth, false); + toStreamNodeWithLetify(out, n[1], depth, true, lbind); out << ')'; return; case kind::DISTINCT: // distinct not supported directly, blast it away with the rewriter - toStream(out, theory::Rewriter::rewrite(n), depth, true); + toStreamNode(out, theory::Rewriter::rewrite(n), depth, true, lbind); return; case kind::SORT_TYPE: { @@ -360,7 +340,9 @@ void CvcPrinter::toStream(std::ostream& out, break; // UF - case kind::APPLY_UF: toStream(op, n.getOperator(), depth, false); break; + case kind::APPLY_UF: + toStreamNode(op, n.getOperator(), depth, false, lbind); + break; case kind::CARDINALITY_CONSTRAINT: case kind::COMBINED_CARDINALITY_CONSTRAINT: out << "CARDINALITY_CONSTRAINT"; @@ -375,14 +357,14 @@ void CvcPrinter::toStream(std::ostream& out, if (i > 1) { out << ", "; } - toStream(out, n[i - 1], depth, false); + toStreamNode(out, n[i - 1], depth, false, lbind); } if (n.getNumChildren() > 2) { out << ')'; } } out << " -> "; - toStream(out, n[n.getNumChildren() - 1], depth, false); + toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind); return; break; @@ -404,7 +386,7 @@ void CvcPrinter::toStream(std::ostream& out, return; break; case kind::APPLY_TYPE_ASCRIPTION: { - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << "::"; TypeNode t = n.getOperator().getConst().getType(); out << (t.isFunctionLike() ? t.getRangeType() : t); @@ -430,14 +412,14 @@ void CvcPrinter::toStream(std::ostream& out, out << ", "; } out << recCons[i].getName() << " := "; - toStream(out, n[i], depth, false); + toStreamNode(out, n[i], depth, false, lbind); } out << " #)"; return; } else { - toStream(op, n.getOperator(), depth, false); + toStreamNode(op, n.getOperator(), depth, false, lbind); if (n.getNumChildren() == 0) { // for datatype constants d, we print "d" and not "d()" @@ -453,11 +435,11 @@ void CvcPrinter::toStream(std::ostream& out, Node opn = n.getOperator(); if (!t.isDatatype()) { - toStream(op, opn, depth, false); + toStreamNode(op, opn, depth, false, lbind); } else if (t.isTuple() || t.isRecord()) { - toStream(out, n[0], depth, true); + toStreamNode(out, n[0], depth, true, lbind); out << '.'; const DType& dt = t.getDType(); if (t.isTuple()) @@ -476,11 +458,11 @@ void CvcPrinter::toStream(std::ostream& out, } else { - toStream(out, opn, depth, false); + toStreamNode(out, opn, depth, false, lbind); } return; }else{ - toStream(op, opn, depth, false); + toStreamNode(op, opn, depth, false, lbind); } } break; @@ -489,7 +471,7 @@ void CvcPrinter::toStream(std::ostream& out, op << "is_"; unsigned cindex = DType::indexOf(n.getOperator()); const DType& dt = DType::datatypeOf(n.getOperator()); - toStream(op, dt[cindex].getConstructor(), depth, false); + toStreamNode(op, dt[cindex].getConstructor(), depth, false, lbind); } break; case kind::CONSTRUCTOR_TYPE: @@ -502,45 +484,45 @@ void CvcPrinter::toStream(std::ostream& out, if(i > 0) { out << ", "; } - toStream(out, n[i], depth, false); + toStreamNode(out, n[i], depth, false, lbind); } if(n.getNumChildren() > 2) { out << ')'; } out << " -> "; } - toStream(out, n[n.getNumChildren() - 1], depth, false); + toStreamNode(out, n[n.getNumChildren() - 1], depth, false, lbind); return; case kind::TESTER_TYPE: - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << " -> BOOLEAN"; return; break; case kind::TUPLE_UPDATE: - toStream(out, n[0], depth, true); + toStreamNode(out, n[0], depth, true, lbind); out << " WITH ." << n.getOperator().getConst().getIndex() << " := "; - toStream(out, n[1], depth, true); + toStreamNode(out, n[1], depth, true, lbind); return; break; case kind::RECORD_UPDATE: - toStream(out, n[0], depth, true); + toStreamNode(out, n[0], depth, true, lbind); out << " WITH ." << n.getOperator().getConst().getField() << " := "; - toStream(out, n[1], depth, true); + toStreamNode(out, n[1], depth, true, lbind); return; break; // ARRAYS case kind::ARRAY_TYPE: out << "ARRAY "; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << " OF "; - toStream(out, n[1], depth, false); + toStreamNode(out, n[1], depth, false, lbind); return; break; case kind::SELECT: - toStream(out, n[0], depth, true); + toStreamNode(out, n[0], depth, true, lbind); out << '['; - toStream(out, n[1], depth, false); + toStreamNode(out, n[1], depth, false, lbind); out << ']'; return; break; @@ -554,18 +536,18 @@ void CvcPrinter::toStream(std::ostream& out, out << '('; } TNode x = stk.top(); - toStream(out, x[0], depth, false); + toStreamNode(out, x[0], depth, false, lbind); out << " WITH ["; - toStream(out, x[1], depth, false); + toStreamNode(out, x[1], depth, false, lbind); out << "] := "; - toStream(out, x[2], depth, false); + toStreamNode(out, x[2], depth, false, lbind); stk.pop(); while(!stk.empty()) { x = stk.top(); out << ", ["; - toStream(out, x[1], depth, false); + toStreamNode(out, x[1], depth, false, lbind); out << "] := "; - toStream(out, x[2], depth, false); + toStreamNode(out, x[2], depth, false, lbind); stk.pop(); } if (bracket) { @@ -651,13 +633,13 @@ void CvcPrinter::toStream(std::ostream& out, else { // ignore, there is no to-real in CVC language - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); } return; } case kind::DIVISIBLE: out << "DIVISIBLE("; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ", " << n.getOperator().getConst().k << ")"; return; @@ -758,16 +740,16 @@ void CvcPrinter::toStream(std::ostream& out, out << "BVPLUS("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, false); + toStreamNode(out, n[child], depth, false, lbind); out << ','; ++child; } out << "BVPLUS("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, false); + toStreamNode(out, n[child], depth, false, lbind); out << ','; - toStream(out, n[child + 1], depth, false); + toStreamNode(out, n[child + 1], depth, false, lbind); while (child > 0) { out << ')'; --child; @@ -781,9 +763,9 @@ void CvcPrinter::toStream(std::ostream& out, Assert(n.getType().isBitVector()); out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ','; - toStream(out, n[1], depth, false); + toStreamNode(out, n[1], depth, false, lbind); out << ')'; return; break; @@ -795,16 +777,16 @@ void CvcPrinter::toStream(std::ostream& out, out << "BVMULT("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, false); + toStreamNode(out, n[child], depth, false, lbind); out << ','; ++child; } out << "BVMULT("; out << BitVectorType(n.getType().toType()).getSize(); out << ','; - toStream(out, n[child], depth, false); + toStreamNode(out, n[child], depth, false, lbind); out << ','; - toStream(out, n[child + 1], depth, false); + toStreamNode(out, n[child + 1], depth, false, lbind); while (child > 0) { out << ')'; --child; @@ -823,31 +805,31 @@ void CvcPrinter::toStream(std::ostream& out, break; case kind::BITVECTOR_REPEAT: out << "BVREPEAT("; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ", " << n.getOperator().getConst() << ')'; return; break; case kind::BITVECTOR_ZERO_EXTEND: out << "BVZEROEXTEND("; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ", " << n.getOperator().getConst() << ')'; return; break; case kind::BITVECTOR_SIGN_EXTEND: out << "SX("; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ", " << BitVectorType(n.getType().toType()).getSize() << ')'; return; break; case kind::BITVECTOR_ROTATE_LEFT: out << "BVROTL("; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ", " << n.getOperator().getConst() << ')'; return; break; case kind::BITVECTOR_ROTATE_RIGHT: out << "BVROTR("; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ", " << n.getOperator().getConst() << ')'; return; break; @@ -855,7 +837,7 @@ void CvcPrinter::toStream(std::ostream& out, // SETS case kind::SET_TYPE: out << "SET OF "; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); return; break; case kind::UNION: @@ -908,7 +890,7 @@ void CvcPrinter::toStream(std::ostream& out, break; case kind::SINGLETON: out << "{"; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << "}"; return; break; @@ -918,13 +900,13 @@ void CvcPrinter::toStream(std::ostream& out, } out << '{'; size_t i = 0; - toStream(out, n[i++], depth, false); + toStreamNode(out, n[i++], depth, false, lbind); for(;i+1 < n.getNumChildren(); ++i) { out << ", "; - toStream(out, n[i], depth, false); + toStreamNode(out, n[i], depth, false, lbind); } out << "} | "; - toStream(out, n[i], depth, true); + toStreamNode(out, n[i], depth, true, lbind); if(bracket) { out << ')'; } @@ -933,7 +915,7 @@ void CvcPrinter::toStream(std::ostream& out, } case kind::CARD: { out << "CARD("; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, false, lbind); out << ")"; return; break; @@ -942,17 +924,17 @@ void CvcPrinter::toStream(std::ostream& out, // Quantifiers case kind::FORALL: out << "(FORALL"; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, true, lbind); out << " : "; - toStream(out, n[1], depth, false); + toStreamNodeWithLetify(out, n[1], depth, true, lbind); out << ')'; // TODO: user patterns? return; case kind::EXISTS: out << "(EXISTS"; - toStream(out, n[0], depth, false); + toStreamNode(out, n[0], depth, true, lbind); out << " : "; - toStream(out, n[1], depth, false); + toStreamNodeWithLetify(out, n[1], depth, true, lbind); out << ')'; // TODO: user patterns? return; @@ -965,7 +947,7 @@ void CvcPrinter::toStream(std::ostream& out, if(i > 0) { out << ", "; } - toStream(out, n[i], -1, false); + toStreamNode(out, n[i], -1, false, lbind); out << ":"; n[i].getType().toStream(out, language::output::LANG_CVC4); } @@ -1021,7 +1003,7 @@ void CvcPrinter::toStream(std::ostream& out, out << ", "; } } - toStream(out, n[i], depth, opType == INFIX); + toStreamNode(out, n[i], depth, opType == INFIX, lbind); } switch (opType) { @@ -1040,8 +1022,7 @@ void CvcPrinter::toStream(std::ostream& out, out << ')' << op.str(); break; } - -}/* CvcPrinter::toStream(TNode) */ +} template static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode); @@ -1611,6 +1592,48 @@ static bool tryToStream(std::ostream& out, return false; } +void CvcPrinter::toStreamNodeWithLetify(std::ostream& out, + Node n, + int toDepth, + bool bracket, + LetBinding* lbind) const +{ + if (lbind == nullptr) + { + toStreamNode(out, n, toDepth, bracket, nullptr); + return; + } + std::vector letList; + lbind->letify(n, letList); + if (!letList.empty()) + { + std::map::const_iterator it; + out << "LET "; + bool first = true; + for (size_t i = 0, nlets = letList.size(); i < nlets; i++) + { + if (!first) + { + out << ", "; + } + else + { + first = false; + } + Node nl = letList[i]; + uint32_t id = lbind->getId(nl); + out << "_let_" << id << " = "; + Node nlc = lbind->convert(nl, "_let_", false); + toStreamNode(out, nlc, toDepth, true, lbind); + } + out << " IN "; + } + Node nc = lbind->convert(n, "_let_"); + // print the body, passing the lbind object + toStreamNode(out, nc, toDepth, bracket, lbind); + lbind->popScope(); +} + }/* CVC4::printer::cvc namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ -- cgit v1.2.3