From 119516a98c052e79ad55e126d13ce1ded38f90af Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Jul 2021 10:30:31 -0500 Subject: [PATCH] Add basic LFSC utilities (#6879) Adds basic utilities in preparation for the LFSC proof conversion. Depends on #6881, review that first. --- src/CMakeLists.txt | 2 + src/proof/lfsc/lfsc_util.cpp | 88 +++++++++++++++++++++++++++++ src/proof/lfsc/lfsc_util.h | 105 +++++++++++++++++++++++++++++++++++ src/proof/proof_rule.cpp | 2 + src/proof/proof_rule.h | 8 +++ 5 files changed, 205 insertions(+) create mode 100644 src/proof/lfsc/lfsc_util.cpp create mode 100644 src/proof/lfsc/lfsc_util.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 2877ab820..9eb7ec3c4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -159,6 +159,8 @@ libcvc5_add_sources( 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 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(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(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 +#include + +#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 "" 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, }; -- 2.30.2