Adds basic utilities in preparation for the LFSC proof conversion.
Depends on #6881, review that first.
proof/lazy_proof_chain.h
proof/lazy_tree_proof_generator.cpp
proof/lazy_tree_proof_generator.h
+ proof/lfsc/lfsc_util.cpp
+ proof/lfsc/lfsc_util.h
proof/method_id.cpp
proof/method_id.h
proof/proof.cpp
--- /dev/null
+/******************************************************************************
+ * 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
--- /dev/null
+/******************************************************************************
+ * 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
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 "?";
// 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,
};
projects / cvc5.git / commitdiff