Add basic LFSC utilities (#6879)

Adds basic utilities in preparation for the LFSC proof conversion.

Depends on #6881, review that first.

4 files changed, 203 insertions, 0 deletions

diff --git a/src/proof/lfsc/lfsc_util.cpp b/src/proof/lfsc/lfsc_util.cpp
new file mode 100644
index 000000000..d8bd8f548
--- /dev/null
+++ b/src/proof/lfsc/lfsc_util.cpp
@@ -0,0 +1,88 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Yoni Zohar
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Utilities for LFSC proofs.
+ */
+
+#include "proof/lfsc/lfsc_util.h"
+
+#include "proof/proof_checker.h"
+#include "util/rational.h"
+
+namespace cvc5 {
+namespace proof {
+
+const char* toString(LfscRule id)
+{
+  switch (id)
+  {
+    case LfscRule::SCOPE: return "scope";
+    case LfscRule::NEG_SYMM: return "neg_symm";
+    case LfscRule::CONG: return "cong";
+    case LfscRule::AND_INTRO1: return "and_intro1";
+    case LfscRule::AND_INTRO2: return "and_intro2";
+    case LfscRule::NOT_AND_REV: return "not_and_rev";
+    case LfscRule::PROCESS_SCOPE: return "process_scope";
+    case LfscRule::ARITH_SUM_UB: return "arith_sum_ub";
+    case LfscRule::INSTANTIATE: return "instantiate";
+    case LfscRule::SKOLEMIZE: return "skolemize";
+    case LfscRule::LAMBDA: return "\\";
+    case LfscRule::PLET: return "plet";
+    default: return "?";
+  }
+}
+std::ostream& operator<<(std::ostream& out, LfscRule id)
+{
+  out << toString(id);
+  return out;
+}
+
+bool getLfscRule(Node n, LfscRule& lr)
+{
+  uint32_t id;
+  if (ProofRuleChecker::getUInt32(n, id))
+  {
+    lr = static_cast<LfscRule>(id);
+    return true;
+  }
+  return false;
+}
+
+LfscRule getLfscRule(Node n)
+{
+  LfscRule lr = LfscRule::UNKNOWN;
+  getLfscRule(n, lr);
+  return lr;
+}
+
+Node mkLfscRuleNode(LfscRule r)
+{
+  return NodeManager::currentNM()->mkConst(Rational(static_cast<uint32_t>(r)));
+}
+
+bool LfscProofLetifyTraverseCallback::shouldTraverse(const ProofNode* pn)
+{
+  if (pn->getRule() == PfRule::SCOPE)
+  {
+    return false;
+  }
+  if (pn->getRule() != PfRule::LFSC_RULE)
+  {
+    return true;
+  }
+  // do not traverse under LFSC (lambda) scope
+  LfscRule lr = getLfscRule(pn->getArguments()[0]);
+  return lr != LfscRule::LAMBDA;
+}
+
+}  // namespace proof
+}  // namespace cvc5
diff --git a/src/proof/lfsc/lfsc_util.h b/src/proof/lfsc/lfsc_util.h
new file mode 100644
index 000000000..c97c07489
--- /dev/null
+++ b/src/proof/lfsc/lfsc_util.h
@@ -0,0 +1,105 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Yoni Zohar
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * Utilities for LFSC proofs.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PROOF__LFSC__LFSC_UTIL_H
+#define CVC5__PROOF__LFSC__LFSC_UTIL_H
+
+#include <iostream>
+#include <map>
+
+#include "expr/node.h"
+#include "proof/proof_letify.h"
+
+namespace cvc5 {
+namespace proof {
+
+/**
+ * LFSC rules. The enum below contains all rules that don't correspond to a
+ * PfRule, e.g. congruence in LFSC does not have the same form as congruence
+ * in the internal calculus.
+ */
+enum class LfscRule : uint32_t
+{
+  //----------- translated rules
+
+  // We defined LFSC versions for rules that either don't exist in the internal
+  // calculus, or have a different set of arugments/children.
+
+  // scope has a different structure, e.g. uses lambdas
+  SCOPE,
+  // must distinguish equalities and disequalities
+  NEG_SYMM,
+  // congruence is done via a higher-order variant of congruence
+  CONG,
+  // we use unrolled binary versions of and intro
+  AND_INTRO1,
+  AND_INTRO2,
+  // needed as a helper for SCOPE
+  NOT_AND_REV,
+  PROCESS_SCOPE,
+  // arithmetic
+  ARITH_SUM_UB,
+
+  // form of quantifier rules varies from internal calculus
+  INSTANTIATE,
+  SKOLEMIZE,
+
+  // a lambda with argument
+  LAMBDA,
+  // a proof-let "plet"
+  PLET,
+  //----------- unknown
+  UNKNOWN,
+};
+
+/**
+ * Converts a lfsc rule to a string. Note: This function is also used in
+ * `safe_print()`. Changing this function name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * @param id The lfsc rule
+ * @return The name of the lfsc rule
+ */
+const char* toString(LfscRule id);
+
+/**
+ * Writes a lfsc rule name to a stream.
+ *
+ * @param out The stream to write to
+ * @param id The lfsc rule to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, LfscRule id);
+/** Get LFSC rule from a node */
+LfscRule getLfscRule(Node n);
+/** Get LFSC rule from a node, return true if success and store in lr */
+bool getLfscRule(Node n, LfscRule& lr);
+/** Make node for LFSC rule */
+Node mkLfscRuleNode(LfscRule r);
+
+/** Helper class used for letifying LFSC proofs. */
+class LfscProofLetifyTraverseCallback : public ProofLetifyTraverseCallback
+{
+ public:
+  bool shouldTraverse(const ProofNode* pn) override;
+};
+
+}  // namespace proof
+}  // namespace cvc5
+
+#endif
diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 27772ce51..3991305ca 100644
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -201,6 +201,8 @@ const char* toString(PfRule id)
       return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
     case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT";
     case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE";
+    //================================================= External rules
+    case PfRule::LFSC_RULE: return "LFSC_RULE";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 6625a1ad8..4b95b47da 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -1389,6 +1389,14 @@ enum class PfRule : uint32_t
   // that extends the Cell and satisfies all assumptions.
   ARITH_NL_CAD_RECURSIVE,
 
+  //================================================ Place holder for Lfsc rules
+  // ======== Lfsc rule
+  // Children: (P1 ... Pn)
+  // Arguments: (id, Q, A1, ..., Am)
+  // ---------------------
+  // Conclusion: (Q)
+  LFSC_RULE,
+
   //================================================= Unknown rule
   UNKNOWN,
 };