From 6d6428a609d76e62cec5ff0ce2bad36e8afe2601 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 19 Nov 2020 15:06:41 -0600 Subject: [PATCH] Use new let binding utility in smt2 printer (#5472) Also fixes some whitespace issues in printing quantified formulas. --- src/printer/smt2/smt2_printer.cpp | 129 +++++++++--------- src/printer/smt2/smt2_printer.h | 20 ++- .../regress0/printer/let_shadowing.smt2 | 4 +- .../regress1/quantifiers/dump-inst-i.smt2 | 8 +- .../regress1/quantifiers/dump-inst-proof.smt2 | 4 +- .../regress1/quantifiers/dump-inst.smt2 | 4 +- 6 files changed, 91 insertions(+), 78 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 9eb5569e3..03b04469c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -31,6 +31,7 @@ #include "options/printer_options.h" #include "options/smt_options.h" #include "printer/dagification_visitor.h" +#include "printer/let_binding.h" #include "proof/unsat_core.h" #include "smt/command.h" #include "smt/node_command.h" @@ -108,51 +109,52 @@ void Smt2Printer::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()) { - theory::SubstitutionMap::const_iterator i = lets.begin(); - theory::SubstitutionMap::const_iterator i_end = lets.end(); - for(; i != i_end; ++ i) { - out << "(let (("; - toStream(out, (*i).second, toDepth); - out << ' '; - toStream(out, (*i).first, toDepth); - out << ")) "; - } - } - Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth); - if(!lets.empty()) { - theory::SubstitutionMap::const_iterator i = lets.begin(); - theory::SubstitutionMap::const_iterator i_end = lets.end(); - for(; i != i_end; ++ i) { - out << ")"; - } - } + LetBinding lbind(dag + 1); + toStreamWithLetify(out, n, toDepth, &lbind); } else { toStream(out, n, toDepth); } } -static bool stringifyRegexp(Node n, stringstream& ss) { - if(n.getKind() == kind::STRING_TO_REGEXP) { - ss << n[0].getConst().toString(true); - } else if(n.getKind() == kind::REGEXP_CONCAT) { - for(unsigned i = 0; i < n.getNumChildren(); ++i) { - if(!stringifyRegexp(n[i], ss)) { - return false; - } - } - } else { - return false; +void Smt2Printer::toStreamWithLetify(std::ostream& out, + Node n, + int toDepth, + LetBinding* lbind) const +{ + if (lbind == nullptr) + { + toStream(out, n, toDepth); + return; } - return true; + std::stringstream cparen; + std::vector letList; + lbind->letify(n, letList); + if (!letList.empty()) + { + std::map::const_iterator it; + for (size_t i = 0, nlets = letList.size(); i < nlets; i++) + { + Node nl = letList[i]; + out << "(let (("; + uint32_t id = lbind->getId(nl); + out << "_let_" << id << " "; + Node nlc = lbind->convert(nl, "_let_", false); + toStream(out, nlc, toDepth, lbind); + out << ")) "; + cparen << ")"; + } + } + Node nc = lbind->convert(n, "_let_"); + // print the body, passing the lbind object + toStream(out, nc, toDepth, lbind); + out << cparen.str(); + lbind->popScope(); } -void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const +void Smt2Printer::toStream(std::ostream& out, + TNode n, + int toDepth, + LetBinding* lbind) const { // null if(n.getKind() == kind::NULL_EXPR) { @@ -486,7 +488,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const << smtKindString(is_int ? kind::TO_INTEGER : kind::DIVISION, d_variant) << " "; - toStream(out, type_asc_arg, toDepth); + toStream(out, type_asc_arg, toDepth, lbind); if (!is_int) { out << " 1"; @@ -498,7 +500,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const { // use type ascription out << "(as "; - toStream(out, type_asc_arg, toDepth < 0 ? toDepth : toDepth - 1); + toStream(out, type_asc_arg, toDepth < 0 ? toDepth : toDepth - 1, lbind); out << " " << force_nt << ")"; } return; @@ -583,20 +585,19 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const args.insert(args.begin(), head[1]); head = head[0]; } - toStream(out, head, toDepth); + toStream(out, head, toDepth, lbind); for (unsigned i = 0, size = args.size(); i < size; ++i) { out << " "; - toStream(out, args[i], toDepth); + toStream(out, args[i], toDepth, lbind); } out << ")"; } return; - case kind::LAMBDA: out << smtKindString(k, d_variant) << " "; break; case kind::MATCH: out << smtKindString(k, d_variant) << " "; - toStream(out, n[0], toDepth); + toStream(out, n[0], toDepth, lbind); out << " ("; for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++) { @@ -604,21 +605,20 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const { out << " "; } - toStream(out, n[i], toDepth); + toStream(out, n[i], toDepth, lbind); } out << "))"; return; case kind::MATCH_BIND_CASE: // ignore the binder - toStream(out, n[1], toDepth); + toStream(out, n[1], toDepth, lbind); out << " "; - toStream(out, n[2], toDepth); + toStream(out, n[2], toDepth, lbind); out << ")"; return; case kind::MATCH_CASE: // do nothing break; - case kind::WITNESS: out << smtKindString(k, d_variant) << " "; break; // arith theory case kind::PLUS: @@ -900,23 +900,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const // quantifiers case kind::FORALL: case kind::EXISTS: + case kind::LAMBDA: + case kind::WITNESS: { - if (k == kind::FORALL) - { - out << "forall "; - } - else - { - out << "exists "; - } - for (unsigned i = 0; i < 2; i++) + out << smtKindString(k, d_variant) << " "; + if (n.getNumChildren() == 3) { - out << n[i] << " "; - if (i == 0 && n.getNumChildren() == 3) - { - out << "(! "; - } + out << "(! "; } + out << n[0] << " "; + toStreamWithLetify(out, n[1], toDepth - 1, lbind); if (n.getNumChildren() == 3) { out << n[2]; @@ -932,7 +925,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;) { out << '('; - toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, 0); + toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1); out << ' '; out << (*i).getType(); out << ')'; @@ -989,7 +982,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const toDepth < 0 ? toDepth : toDepth - 1); } }else{ - toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1); + toStream( + out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind); } } else { out << "(...)"; @@ -1002,7 +996,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, int toDepth) const for(size_t i = 0, c = 1; i < n.getNumChildren(); ) { if(toDepth != 0) { - toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - c); + toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - c, lbind); } else { out << "(...)"; } @@ -1062,8 +1056,7 @@ static string smtKindString(Kind k, Variant v) // uf theory case kind::APPLY_UF: break; - case kind::LAMBDA: - return "lambda"; + case kind::LAMBDA: return "lambda"; case kind::MATCH: return "match"; case kind::WITNESS: return "witness"; @@ -1279,6 +1272,10 @@ static string smtKindString(Kind k, Variant v) case kind::SEP_WAND: return "wand"; case kind::SEP_EMP: return "emp"; + // quantifiers + case kind::FORALL: return "forall"; + case kind::EXISTS: return "exists"; + default: ; /* fall through */ } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index bc8674275..c83a74d97 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -22,6 +22,9 @@ #include "printer/printer.h" namespace CVC4 { + +class LetBinding; + namespace printer { namespace smt2 { @@ -224,7 +227,13 @@ class Smt2Printer : public CVC4::Printer std::ostream& out, const std::vector& sequence) const override; private: - void toStream(std::ostream& out, TNode n, int toDepth) const; + /** + * The main printing method for nodes n. + */ + void toStream(std::ostream& out, + TNode n, + int toDepth, + LetBinding* lbind = nullptr) const; /** * To stream, with a forced type. This method is used in some corner cases * to force a node n to be printed as if it had type tn. This is used e.g. @@ -239,7 +248,14 @@ class Smt2Printer : public CVC4::Printer const NodeCommand* c) const override; void toStream(std::ostream& out, const SExpr& sexpr) const; void toStream(std::ostream& out, const DType& dt) const; - + /** + * To stream with let binding. This prints n, possibly in the scope + * of letification generated by this method based on lbind. + */ + void toStreamWithLetify(std::ostream& out, + Node n, + int toDepth, + LetBinding* lbind) const; Variant d_variant; }; /* class Smt2Printer */ diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2 index 017479871..14f2316a7 100644 --- a/test/regress/regress0/printer/let_shadowing.smt2 +++ b/test/regress/regress0/printer/let_shadowing.smt2 @@ -2,8 +2,8 @@ ; COMMAND-LINE: --dump raw-benchmark --preprocess-only ; SCRUBBER: grep assert ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0)))) -; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0) ))))) -; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))) ) ))))) +; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0)))))) +; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))))))))) (set-logic NIA) (declare-const _let_0 Int) (declare-const x Int) diff --git a/test/regress/regress1/quantifiers/dump-inst-i.smt2 b/test/regress/regress1/quantifiers/dump-inst-i.smt2 index 8a9f10ea7..fab0e3f0c 100644 --- a/test/regress/regress1/quantifiers/dump-inst-i.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst-i.smt2 @@ -1,17 +1,17 @@ ; COMMAND-LINE: --dump-instantiations --incremental --print-inst-full ; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' ; EXPECT: unsat -; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x))) ; EXPECT: ( skv_TERM ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (P x) ) +; EXPECT: (instantiations (forall ((x Int)) (P x)) ; EXPECT: ( skv_TERM ) ; EXPECT: ) ; EXPECT: unsat -; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x)) ) +; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x))) ; EXPECT: ( skv_TERM ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (P x) ) +; EXPECT: (instantiations (forall ((x Int)) (P x)) ; EXPECT: ( skv_TERM ) ; EXPECT: ) (set-logic UFLIA) diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 index f900e78a9..274fc213f 100644 --- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 @@ -1,10 +1,10 @@ ; REQUIRES: proof ; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full ; EXPECT: unsat -; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x))) ; EXPECT: ( 2 ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))) ) +; EXPECT: (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x)))) ; EXPECT: ( 2 ) ; EXPECT: ) (set-logic UFLIA) diff --git a/test/regress/regress1/quantifiers/dump-inst.smt2 b/test/regress/regress1/quantifiers/dump-inst.smt2 index d15025900..6ded98602 100644 --- a/test/regress/regress1/quantifiers/dump-inst.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst.smt2 @@ -1,10 +1,10 @@ ; COMMAND-LINE: --dump-instantiations --print-inst-full ; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' ; EXPECT: unsat -; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x))) ; EXPECT: ( skv_TERM ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (P x) ) +; EXPECT: (instantiations (forall ((x Int)) (P x)) ; EXPECT: ( skv_TERM ) ; EXPECT: ) (set-logic UFLIA) -- 2.30.2