Use new let binding utility in smt2 printer (#5472)

Also fixes some whitespace issues in printing quantified formulas.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9eb5569e30b08b21ec31919e5df52cb97baa5cb8..03b04469cc45e6f83a9f4369ff007a6e3ebf87e9 100644 (file)
--- 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<DagificationVisitor> 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<String>().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<Node> letList;
+  lbind->letify(n, letList);
+  if (!letList.empty())
+  {
+    std::map<Node, uint32_t>::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 bc867427562758863ef8120e577cb7fe782f5c24..c83a74d97faeabcf2d274ecf38b99328dd71e26b 100644 (file)
--- 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<Command*>& 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 0174798719cacb4b4ddfe3adca24470c8bbd45d9..14f2316a7504d740813153dc3360de2d3a91544a 100644 (file)
--- 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 8a9f10ea7a49832cffd4cfb059e1d799aea7cbe7..fab0e3f0ca0403c5b9c04e944eebdc5d6f33e532 100644 (file)
--- 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 f900e78a95e1910a0675f173ac9b9af094260672..274fc213f745c84f3751ed2b1636745ab891136f 100644 (file)
--- 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 d150259006f0798b88b29109bd8b7966569e2146..6ded98602932f6f73927cdfb4e45393c646f7a26 100644 (file)
--- 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)