Merge branch 'master' into rmStateOptionsrmStateOptions

12 files changed, 306 insertions, 97 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5c898b654..4484f9447 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -182,6 +182,8 @@ libcvc5_add_sources(
   proof/lfsc/lfsc_list_sc_node_converter.h
   proof/lfsc/lfsc_node_converter.cpp
   proof/lfsc/lfsc_node_converter.h
+  proof/lfsc/lfsc_print_channel.cpp
+  proof/lfsc/lfsc_print_channel.h
   proof/lfsc/lfsc_util.cpp
   proof/lfsc/lfsc_util.h
   proof/method_id.cpp
diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp
new file mode 100644
index 000000000..36fd8831b
--- /dev/null
+++ b/src/proof/lfsc/lfsc_print_channel.cpp
@@ -0,0 +1,161 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Print channels for LFSC proofs.
+ */
+
+#include "proof/lfsc/lfsc_print_channel.h"
+
+#include <sstream>
+
+#include "proof/lfsc/lfsc_util.h"
+
+namespace cvc5 {
+namespace proof {
+
+LfscPrintChannelOut::LfscPrintChannelOut(std::ostream& out) : d_out(out) {}
+void LfscPrintChannelOut::printNode(TNode n)
+{
+  d_out << " ";
+  printNodeInternal(d_out, n);
+}
+
+void LfscPrintChannelOut::printTypeNode(TypeNode tn)
+{
+  d_out << " ";
+  printTypeNodeInternal(d_out, tn);
+}
+
+void LfscPrintChannelOut::printHole() { d_out << " _ "; }
+void LfscPrintChannelOut::printTrust(TNode res, PfRule src)
+{
+  d_out << std::endl << "(trust ";
+  printNodeInternal(d_out, res);
+  d_out << ") ; from " << src << std::endl;
+}
+
+void LfscPrintChannelOut::printOpenRule(const ProofNode* pn)
+{
+  d_out << std::endl << "(";
+  printRule(d_out, pn);
+}
+
+void LfscPrintChannelOut::printOpenLfscRule(LfscRule lr)
+{
+  d_out << std::endl << "(" << lr;
+}
+
+void LfscPrintChannelOut::printCloseRule(size_t nparen)
+{
+  for (size_t i = 0; i < nparen; i++)
+  {
+    d_out << ")";
+  }
+}
+
+void LfscPrintChannelOut::printProofId(size_t id)
+{
+  d_out << " ";
+  printProofId(d_out, id);
+}
+void LfscPrintChannelOut::printAssumeId(size_t id)
+{
+  d_out << " ";
+  printAssumeId(d_out, id);
+}
+
+void LfscPrintChannelOut::printEndLine() { d_out << std::endl; }
+
+void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n)
+{
+  // due to use of special names in the node converter, we must clean symbols
+  std::stringstream ss;
+  n.toStream(ss, -1, 0, Language::LANG_SMTLIB_V2_6);
+  std::string s = ss.str();
+  cleanSymbols(s);
+  out << s;
+}
+
+void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn)
+{
+  // due to use of special names in the node converter, we must clean symbols
+  std::stringstream ss;
+  tn.toStream(ss, Language::LANG_SMTLIB_V2_6);
+  std::string s = ss.str();
+  cleanSymbols(s);
+  out << s;
+}
+
+void LfscPrintChannelOut::printRule(std::ostream& out, const ProofNode* pn)
+{
+  if (pn->getRule() == PfRule::LFSC_RULE)
+  {
+    const std::vector<Node>& args = pn->getArguments();
+    out << getLfscRule(args[0]);
+    return;
+  }
+  // Otherwise, convert to lower case
+  std::stringstream ss;
+  ss << pn->getRule();
+  std::string rname = ss.str();
+  std::transform(
+      rname.begin(), rname.end(), rname.begin(), [](unsigned char c) {
+        return std::tolower(c);
+      });
+  out << rname;
+}
+
+void LfscPrintChannelOut::printId(std::ostream& out, size_t id)
+{
+  out << "__t" << id;
+}
+
+void LfscPrintChannelOut::printProofId(std::ostream& out, size_t id)
+{
+  out << "__p" << id;
+}
+
+void LfscPrintChannelOut::printAssumeId(std::ostream& out, size_t id)
+{
+  out << "__a" << id;
+}
+
+void LfscPrintChannelOut::cleanSymbols(std::string& s)
+{
+  size_t start_pos = 0;
+  while ((start_pos = s.find("(_ ", start_pos)) != std::string::npos)
+  {
+    s.replace(start_pos, 3, "(");
+    start_pos += 1;
+  }
+  start_pos = 0;
+  while ((start_pos = s.find("__LFSC_TMP", start_pos)) != std::string::npos)
+  {
+    s.replace(start_pos, 10, "");
+  }
+}
+
+LfscPrintChannelPre::LfscPrintChannelPre(LetBinding& lbind) : d_lbind(lbind) {}
+
+void LfscPrintChannelPre::printNode(TNode n) { d_lbind.process(n); }
+void LfscPrintChannelPre::printTrust(TNode res, PfRule src)
+{
+  d_lbind.process(res);
+}
+
+void LfscPrintChannelPre::printOpenRule(const ProofNode* pn)
+{
+
+}
+
+}  // namespace proof
+}  // namespace cvc5
diff --git a/src/proof/lfsc/lfsc_print_channel.h b/src/proof/lfsc/lfsc_print_channel.h
new file mode 100644
index 000000000..655fa192c
--- /dev/null
+++ b/src/proof/lfsc/lfsc_print_channel.h
@@ -0,0 +1,128 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Print channels for LFSC proofs.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H
+#define CVC4__PROOF__LFSC__LFSC_PRINT_CHANNEL_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "printer/let_binding.h"
+#include "proof/lfsc/lfsc_util.h"
+#include "proof/proof_node.h"
+
+namespace cvc5 {
+namespace proof {
+
+/**
+ * LFSC proofs are printed in two phases: the first phase computes the
+ * letification of terms in the proof as well as other information that is
+ * required for printing the preamble of the proof. The second phase prints the
+ * proof to an output stream. This is the base class for these two phases.
+ */
+class LfscPrintChannel
+{
+ public:
+  LfscPrintChannel() {}
+  virtual ~LfscPrintChannel() {}
+  /** Print node n */
+  virtual void printNode(TNode n) {}
+  /** Print type node n */
+  virtual void printTypeNode(TypeNode tn) {}
+  /** Print a hole */
+  virtual void printHole() {}
+  /**
+   * Print an application of the trusting the result res, whose source is the
+   * given proof rule.
+   */
+  virtual void printTrust(TNode res, PfRule src) {}
+  /** Print the opening of the rule of proof rule pn, e.g. "(and_elim ". */
+  virtual void printOpenRule(const ProofNode* pn) {}
+  /** Print the opening of LFSC rule lr, e.g. "(cong " */
+  virtual void printOpenLfscRule(LfscRule lr) {}
+  /** Print the closing of # nparen proof rules */
+  virtual void printCloseRule(size_t nparen = 1) {}
+  /** Print a letified proof with the given identifier */
+  virtual void printProofId(size_t id) {}
+  /** Print a proof assumption with the given identifier */
+  virtual void printAssumeId(size_t id) {}
+  /** Print an end line */
+  virtual void printEndLine() {}
+};
+
+/** Prints the proof to output stream d_out */
+class LfscPrintChannelOut : public LfscPrintChannel
+{
+ public:
+  LfscPrintChannelOut(std::ostream& out);
+  void printNode(TNode n) override;
+  void printTypeNode(TypeNode tn) override;
+  void printHole() override;
+  void printTrust(TNode res, PfRule src) override;
+  void printOpenRule(const ProofNode* pn) override;
+  void printOpenLfscRule(LfscRule lr) override;
+  void printCloseRule(size_t nparen = 1) override;
+  void printProofId(size_t id) override;
+  void printAssumeId(size_t id) override;
+  void printEndLine() override;
+  //------------------- helper methods
+  /**
+   * Print node to stream in the expected format of LFSC.
+   */
+  static void printNodeInternal(std::ostream& out, Node n);
+  /**
+   * Print type node to stream in the expected format of LFSC.
+   */
+  static void printTypeNodeInternal(std::ostream& out, TypeNode tn);
+  static void printRule(std::ostream& out, const ProofNode* pn);
+  static void printId(std::ostream& out, size_t id);
+  static void printProofId(std::ostream& out, size_t id);
+  static void printAssumeId(std::ostream& out, size_t id);
+  //------------------- end helper methods
+ private:
+  /**
+   * Replaces "(_ " with "(" to eliminate indexed symbols
+   * Replaces "__LFSC_TMP" with ""
+   */
+  static void cleanSymbols(std::string& s);
+  /** The output stream */
+  std::ostream& d_out;
+};
+
+/**
+ * Run on the proof before it is printed, and does two preparation steps:
+ * - Computes the letification of nodes that appear in the proof.
+ * - Computes the set of DSL rules that appear in the proof.
+ */
+class LfscPrintChannelPre : public LfscPrintChannel
+{
+ public:
+  LfscPrintChannelPre(LetBinding& lbind);
+  void printNode(TNode n) override;
+  void printTrust(TNode res, PfRule src) override;
+  void printOpenRule(const ProofNode* pn) override;
+
+ private:
+  /** The let binding */
+  LetBinding& d_lbind;
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 8d1bfd9b6..708bffe80 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -345,7 +345,7 @@ void Cegis::addRefinementLemma(Node lem)
                           d_rl_vals.end());
   }
   // rewrite with extended rewriter
-  slem = extendedRewrite(slem);
+  slem = d_tds->rewriteNode(slem);
   // collect all variables in slem
   expr::getSymbols(slem, d_refinement_lemma_vars);
   std::vector<Node> waiting;
@@ -509,7 +509,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
       Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end());
       Trace("sygus-cref-eval2")
           << "...under substitution it is : " << lemcs << std::endl;
-      Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs);
+      Node lemcsu = d_tds->rewriteNode(lemcs);
       Trace("sygus-cref-eval2")
           << "...after unfolding is : " << lemcsu << std::endl;
       if (lemcsu.isConst() && !lemcsu.getConst<bool>())
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 0ef1e7f17..7af1ef45b 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -180,7 +180,7 @@ void SygusEvalUnfold::registerModelValue(Node a,
           Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children);
           eval_children[0] = vn;
           Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
-          res = d_tds->evaluateWithUnfolding(eval_fun);
+          res = d_tds->rewriteNode(eval_fun);
           Trace("sygus-eval-unfold")
               << "Evaluate with unfolding returns " << res << std::endl;
           esit.init(conj, n, res);
@@ -324,13 +324,6 @@ Node SygusEvalUnfold::unfold(Node en,
   return ret;
 }
 
-Node SygusEvalUnfold::unfold(Node en)
-{
-  std::map<Node, Node> vtm;
-  std::vector<Node> exp;
-  return unfold(en, vtm, exp, false, false);
-}
-
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
index bb181996a..c30d4dae7 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
@@ -122,11 +122,6 @@ class SygusEvalUnfold
               std::vector<Node>& exp,
               bool track_exp = true,
               bool doRec = false);
-  /**
-   * Same as above, but without explanation tracking. This is used for concrete
-   * evaluation heads
-   */
-  Node unfold(Node en);
 
  private:
   /** sygus term database associated with this utility */
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 29557fe5c..8048330e4 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -49,11 +49,6 @@ void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
   d_result = res;
 }
 
-Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n)
-{
-  return tds->evaluateWithUnfolding(n, d_visited);
-}
-
 bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
 {
   TNode tnvn = nvn;
@@ -61,7 +56,7 @@ bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
   for (const Node& c : d_terms)
   {
     Node conj_subs = c.substitute(d_var, tnvn, cache);
-    Node conj_subs_unfold = doEvaluateWithUnfolding(tds, conj_subs);
+    Node conj_subs_unfold = tds->rewriteNode(conj_subs);
     Trace("sygus-cref-eval2-debug")
         << "  ...check unfolding : " << conj_subs_unfold << std::endl;
     Trace("sygus-cref-eval2-debug")
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index ca5f057b1..afb59bf73 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -111,9 +111,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest
    */
   void init(Node conj, Node var, Node res);
 
-  /** do evaluate with unfolding, using the cache of this class */
-  Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n);
-
  protected:
   /** does d_terms{ d_var -> nvn } still rewrite to d_result? */
   bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
@@ -137,8 +134,6 @@ class EvalSygusInvarianceTest : public SygusInvarianceTest
    * disjunctively, i.e. if one child test succeeds, the overall test succeeds.
    */
   bool d_is_conjunctive;
-  /** cache of n -> the simplified form of eval( n ) */
-  std::unordered_map<Node, Node> d_visited;
 };
 
 /** EquivSygusInvarianceTest
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index bcd826799..b7611784d 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -444,7 +444,7 @@ Node SygusRepairConst::getFoQuery(Node body,
   Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;
 
   Trace("sygus-repair-const") << "  Unfold the specification..." << std::endl;
-  body = d_tds->evaluateWithUnfolding(body);
+  body = d_tds->rewriteNode(body);
   Trace("sygus-repair-const-debug") << "  ...got : " << body << std::endl;
 
   Trace("sygus-repair-const") << "  Introduce first-order vars..." << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 10db1ef9e..6b023075b 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -264,7 +264,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
     Trace("sygus-unif-debug2") << "  Test evaluation of " << eut << "..."
                                << std::endl;
-    eut = d_tds->getEvalUnfold()->unfold(eut);
+    eut = d_tds->rewriteNode(eut);
     Trace("sygus-unif-debug2") << "  ...got " << eut;
     Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 9c9a90255..035db433e 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -739,7 +739,15 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
 
 Node TermDbSygus::rewriteNode(Node n) const
 {
-  Node res = Rewriter::rewrite(n);
+  Node res;
+  if (options().quantifiers.sygusExtRew)
+  {
+    res = extendedRewrite(n);
+  }
+  else
+  {
+    res = rewrite(n);
+  }
   if (res.isConst())
   {
     // constant, we are done
@@ -1001,59 +1009,6 @@ Node TermDbSygus::evaluateBuiltin(TypeNode tn,
   return rewriteNode(res);
 }
 
-Node TermDbSygus::evaluateWithUnfolding(Node n,
-                                        std::unordered_map<Node, Node>& visited)
-{
-  std::unordered_map<Node, Node>::iterator it = visited.find(n);
-  if( it==visited.end() ){
-    Node ret = n;
-    while (ret.getKind() == DT_SYGUS_EVAL
-           && ret[0].getKind() == APPLY_CONSTRUCTOR)
-    {
-      if (ret == n && ret[0].isConst())
-      {
-        // use rewriting, possibly involving recursive functions
-        ret = rewriteNode(ret);
-      }
-      else
-      {
-        ret = d_eval_unfold->unfold(ret);
-      }
-    }    
-    if( ret.getNumChildren()>0 ){
-      std::vector< Node > children;
-      if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( ret.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<ret.getNumChildren(); i++ ){
-        Node nc = evaluateWithUnfolding(ret[i], visited);
-        childChanged = childChanged || nc!=ret[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( ret.getKind(), children );
-      }
-      if (options::sygusExtRew())
-      {
-        ret = extendedRewrite(ret);
-      }
-      // use rewriting, possibly involving recursive functions
-      ret = rewriteNode(ret);
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
-}
-
-Node TermDbSygus::evaluateWithUnfolding(Node n)
-{
-  std::unordered_map<Node, Node> visited;
-  return evaluateWithUnfolding(n, visited);
-}
-
 bool TermDbSygus::isEvaluationPoint(Node n) const
 {
   if (n.getKind() != DT_SYGUS_EVAL)
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index a44ebd297..7b05c70e4 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -271,21 +271,6 @@ class TermDbSygus : protected EnvObj
                        Node bn,
                        const std::vector<Node>& args,
                        bool tryEval = true);
-  /** evaluate with unfolding
-   *
-   * n is any term that may involve sygus evaluation functions. This function
-   * returns the result of unfolding the evaluation functions within n and
-   * rewriting the result. For example, if eval_A is the evaluation function
-   * for the datatype:
-   *   A -> C_0 | C_1 | C_x | C_+( C_A, C_A )
-   * corresponding to grammar:
-   *   A -> 0 | 1 | x | A + A
-   * then calling this function on eval( C_+( x, 1 ), 4 ) = y returns 5 = y.
-   * The node returned by this function is in (extended) rewritten form.
-   */
-  Node evaluateWithUnfolding(Node n);
-  /** same as above, but with a cache of visited nodes */
-  Node evaluateWithUnfolding(Node n, std::unordered_map<Node, Node>& visited);
   /** is evaluation point?
    *
    * Returns true if n is of the form eval( x, c1...cn ) for some variable x