Disallow let in sygus grammars, check for free variables in sygus constructors (#3259)

2 files changed, 0 insertions, 112 deletions

diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index e320d5dfd..2b6d5fc1e 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -96,79 +96,6 @@ void SygusExprPrintCallback::toStreamSygus(const Printer* p,
   }
 }
 
-SygusLetExprPrintCallback::SygusLetExprPrintCallback(
-    Expr let_body, std::vector<Expr>& let_args, unsigned ninput_args)
-    : SygusExprPrintCallback(let_body, let_args),
-      d_num_let_input_args(ninput_args)
-{
-}
-
-void SygusLetExprPrintCallback::toStreamSygus(const Printer* p,
-                                              std::ostream& out,
-                                              Expr e) const
-{
-  std::stringstream let_out;
-  // print as let term
-  if (d_num_let_input_args > 0)
-  {
-    let_out << "(let (";
-  }
-  std::vector<Node> subs_lvs;
-  std::vector<Node> new_lvs;
-  for (unsigned i = 0, size = d_args.size(); i < size; i++)
-  {
-    Node v = d_args[i];
-    subs_lvs.push_back(v);
-    std::stringstream ss;
-    ss << "_l_" << new_lvs.size();
-    Node lv = NodeManager::currentNM()->mkBoundVar(ss.str(), v.getType());
-    new_lvs.push_back(lv);
-    // map free variables to proper terms
-    if (i < d_num_let_input_args)
-    {
-      // it should be printed as a let argument
-      let_out << "(";
-      let_out << lv << " " << lv.getType() << " ";
-      p->toStreamSygus(let_out, e[i]);
-      let_out << ")";
-    }
-  }
-  if (d_num_let_input_args > 0)
-  {
-    let_out << ") ";
-  }
-  // print the body
-  Node slet_body = Node::fromExpr(d_body);
-  slet_body = slet_body.substitute(
-      subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end());
-  // new_lvs.insert(new_lvs.end(), lvs.begin(), lvs.end());
-  p->toStreamSygus(let_out, slet_body);
-  if (d_num_let_input_args > 0)
-  {
-    let_out << ")";
-  }
-  // do variable substitutions since
-  // ASSUMING : let_vars are interpreted literally and do not represent a class
-  // of variables
-  std::string lbody = let_out.str();
-  for (unsigned i = 0, size = d_args.size(); i < size; i++)
-  {
-    std::stringstream old_str;
-    old_str << new_lvs[i];
-    std::stringstream new_str;
-    if (i >= d_num_let_input_args)
-    {
-      p->toStreamSygus(new_str, Node::fromExpr(e[i]));
-    }
-    else
-    {
-      new_str << d_args[i];
-    }
-    doStrReplace(lbody, old_str.str().c_str(), new_str.str().c_str());
-  }
-  out << lbody;
-}
-
 SygusNamedPrintCallback::SygusNamedPrintCallback(std::string name)
     : d_name(name)
 {
diff --git a/src/printer/sygus_print_callback.h b/src/printer/sygus_print_callback.h
index d956fd4c6..d10a312bd 100644
--- a/src/printer/sygus_print_callback.h
+++ b/src/printer/sygus_print_callback.h
@@ -68,45 +68,6 @@ class CVC4_PUBLIC SygusExprPrintCallback : public SygusPrintCallback
                     const std::string& newStr) const;
 };
 
-/** sygus let expression constructor printer
- *
- * This class is used for printing sygus
- * datatype constructor terms whose top symbol
- * is a let expression.
- * For example, for grammar:
- *   A -> (let ((x B)) (+ A 1)) | x | (+ A A) | 0
- *   B -> 0 | 1
- * the first constructor for A takes as arguments
- * (B,A) and has sygus operator
- *   (lambda ((y Int) (z Int)) (+ z 1))
- * CVC4's support for let expressions in grammars
- * is highly limited, since notice that the
- * argument y : B is unused.
- *
- * For the above constructor, we have that
- *   d_let_body is (+ z 1),
- *   d_sygus_let_args is { y, z },
- *   d_sygus_num_let_input_args is 1, since
- *     y is an original input argument of the
- *     let expression, but z is not.
- */
-class CVC4_PUBLIC SygusLetExprPrintCallback : public SygusExprPrintCallback
-{
- public:
-  SygusLetExprPrintCallback(Expr let_body,
-                            std::vector<Expr>& let_args,
-                            unsigned ninput_args);
-  ~SygusLetExprPrintCallback() {}
-  /** print sygus term e on output out using printer p */
-  virtual void toStreamSygus(const Printer* p,
-                             std::ostream& out,
-                             Expr e) const override;
-
- private:
-  /** number of arguments that are interpreted as input arguments */
-  unsigned d_num_let_input_args;
-};
-
 /** sygus named constructor printer
  *
  * This callback is used for explicitly naming