Add LFSC side condition conversion utility for list variables (#7131)

Required for automatic generation of side conditions from DSL rewrite rules.

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index a25d287a94364b56243cb3fc59cda9a309a3efd8..ba88080b8bfc47f1e720afcbf7318bafffcbc1c9 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -178,6 +178,8 @@ libcvc5_add_sources(
   proof/lazy_proof_chain.h
   proof/lazy_tree_proof_generator.cpp
   proof/lazy_tree_proof_generator.h
+  proof/lfsc/lfsc_list_sc_node_converter.cpp
+  proof/lfsc/lfsc_list_sc_node_converter.h
   proof/lfsc/lfsc_node_converter.cpp
   proof/lfsc/lfsc_node_converter.h
   proof/lfsc/lfsc_util.cpp

diff --git a/src/proof/lfsc/lfsc_list_sc_node_converter.cpp b/src/proof/lfsc/lfsc_list_sc_node_converter.cpp
new file mode 100644 (file)
index 0000000..bf72fb8
--- /dev/null
+++ b/src/proof/lfsc/lfsc_list_sc_node_converter.cpp
@@ -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.
+ * ****************************************************************************
+ *
+ * Implementation of LFSC node conversion for list variables in side conditions
+ */
+
+#include "proof/lfsc/lfsc_list_sc_node_converter.h"
+
+namespace cvc5 {
+namespace proof {
+
+LfscListScNodeConverter::LfscListScNodeConverter(
+    LfscNodeConverter& conv,
+    const std::unordered_set<Node>& listVars,
+    bool isPre)
+    : d_conv(conv), d_listVars(listVars), d_isPre(isPre)
+{
+}
+
+Node LfscListScNodeConverter::postConvert(Node n)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Kind k = n.getKind();
+  if (d_isPre)
+  {
+    // is this an application that may require nary elimination?
+    if (NodeManager::isNAryKind(k))
+    {
+      size_t minLength = 0;
+      for (const Node& nc : n)
+      {
+        if (d_listVars.find(nc) == d_listVars.end())
+        {
+          minLength++;
+          if (minLength >= 2)
+          {
+            // no need to convert
+            return n;
+          }
+        }
+      }
+      TypeNode tn = n.getType();
+      // if so, (or a b c) becomes (nary_elim f_or (or a b c) false),
+      // where the children of this are converted
+      std::vector<Node> children;
+      Node f = d_conv.getOperatorOfTerm(n);
+      children.push_back(f);
+      // convert n, since this node will not be converted further
+      children.push_back(d_conv.convert(n));
+      Node null = d_conv.getNullTerminator(k, tn);
+      Assert(!null.isNull());
+      // likewise, convert null
+      children.push_back(d_conv.convert(null));
+      Node sop = mkOperatorFor("nary_elim", children, tn);
+      children.insert(children.begin(), sop);
+      return nm->mkNode(kind::APPLY_UF, children);
+    }
+    return n;
+  }
+  Assert(k == kind::APPLY_UF || k == kind::APPLY_CONSTRUCTOR
+         || !NodeManager::isNAryKind(k) || n.getNumChildren() == 2)
+      << "Cannot convert LFSC side condition for " << n;
+  // note that after converting to binary form, variables should only appear
+  // as the first child of binary applications of n-ary operators
+  if (n.getNumChildren() == 2 && d_listVars.find(n[0]) != d_listVars.end())
+  {
+    // this will fail if e.g. a list variable is a child of a non-n-ary kind
+    Assert(NodeManager::isNAryKind(k));
+    TypeNode tn = n.getType();
+    // We are in converted form, but need to get the null terminator for the
+    // original term. Hence, we convert the application back to original form
+    // if we replaced with an APPLY_UF.
+    if (k == kind::APPLY_UF)
+    {
+      k = d_conv.getBuiltinKindForInternalSymbol(n.getOperator());
+      Assert(k != kind::UNDEFINED_KIND);
+      // for uniformity, reconstruct in original form
+      std::vector<Node> nchildren(n.begin(), n.end());
+      n = nm->mkNode(k, nchildren);
+    }
+    Node null = d_conv.getNullTerminator(k, tn);
+    AlwaysAssert(!null.isNull())
+        << "No null terminator for " << k << ", " << tn;
+    null = d_conv.convert(null);
+    // if a list variable occurs as a rightmost child, then we return just
+    // the variable
+    if (n[1] == null)
+    {
+      return n[0];
+    }
+    // E.g. (or x t) becomes (nary_concat f_or x t false)
+    std::vector<Node> children;
+    Node f = d_conv.getOperatorOfTerm(n);
+    children.push_back(f);
+    children.insert(children.end(), n.begin(), n.end());
+    children.push_back(null);
+    Node sop = mkOperatorFor("nary_concat", children, tn);
+    children.insert(children.begin(), sop);
+    return nm->mkNode(kind::APPLY_UF, children);
+  }
+  return n;
+}
+
+Node LfscListScNodeConverter::mkOperatorFor(const std::string& name,
+                                            const std::vector<Node>& children,
+                                            TypeNode retType)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<TypeNode> childTypes;
+  for (const Node& c : children)
+  {
+    childTypes.push_back(c.getType());
+  }
+  TypeNode ftype = nm->mkFunctionType(childTypes, retType);
+  return d_conv.mkInternalSymbol(name, ftype);
+}
+
+}  // namespace proof
+}  // namespace cvc5

diff --git a/src/proof/lfsc/lfsc_list_sc_node_converter.h b/src/proof/lfsc/lfsc_list_sc_node_converter.h
new file mode 100644 (file)
index 0000000..fe0f188
--- /dev/null
+++ b/src/proof/lfsc/lfsc_list_sc_node_converter.h
@@ -0,0 +1,86 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Implementation of LFSC node conversion for list variables in side conditions
+ */
+#include "cvc5_private.h"
+
+#ifndef CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H
+#define CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H
+
+#include "expr/node_converter.h"
+#include "proof/lfsc/lfsc_node_converter.h"
+
+namespace cvc5 {
+namespace proof {
+
+/**
+ * Convert list variables in side conditions. This class converts nodes
+ * representing LFSC side condition programs to a form that prints properly
+ * in LFSC. In particular, this node converter gives consideration to
+ * input variables that are "list" variables in the rewrite DSL.
+ *
+ * For example, for DSL rule:
+ *   (define-rule bool-and-flatten
+ *      ((xs Bool :list) (b Bool) (ys Bool :list) (zs Bool :list))
+ *      (and xs (and b ys) zs) (and xs zs b ys))
+ * This is a helper class used to compute the conclusion of this rule. This
+ * class is used to turn
+ *   (= (and xs (and b ys) zs) (and xs zs b ys))
+ * into:
+ *   (=
+ *      (nary_concat
+ *        f_and
+ *        xs
+ *        (and (and b ys) zs)
+ *        true)
+ *      (nary_elim
+ *        f_and
+ *        (nary_concat f_and xs (nary_concat f_and zs (and b ys) true) true)
+ *        true)))
+ * Where notice that the list variables xs, ys, zs are treated as lists to
+ * concatenate instead of being subterms, according to the semantics of list
+ * variables in the rewrite DSL. For exact definitions of nary_elim,
+ * nary_concat, see the LFSC signature nary_programs.plf.
+ *
+ * This runs in two modes.
+ * - If isPre is true, then the input is in its original form, and we add
+ * applications of nary_elim.
+ * - If isPre is false, then the input is in converted form, and we add
+ * applications of nary_concat.
+ */
+class LfscListScNodeConverter : public NodeConverter
+{
+ public:
+  LfscListScNodeConverter(LfscNodeConverter& conv,
+                          const std::unordered_set<Node>& listVars,
+                          bool isPre = false);
+  /** convert to internal */
+  Node postConvert(Node n) override;
+
+ private:
+  /** Make application for */
+  Node mkOperatorFor(const std::string& name,
+                     const std::vector<Node>& children,
+                     TypeNode retType);
+  /** The parent converter, used for getting internal symbols and utilities */
+  LfscNodeConverter& d_conv;
+  /** Variables we are treating as list variables */
+  std::unordered_set<Node> d_listVars;
+  /** In pre or post */
+  bool d_isPre;
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif