From c4f5de386f7ac59d866bafe4a191fd986ca77d26 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Apr 2024 09:49:03 -0500 Subject: [PATCH] Rename REMOVE_TERM_FORMULA_AXIOM to ITE_EQ (#10704) Also makes the documentation explicitly given. --- include/cvc5/cvc5_proof_rule.h | 6 +++--- proofs/alf/cvc5/rules/Builtin.smt3 | 2 +- src/api/cpp/cvc5_proof_rule_template.cpp | 3 +-- src/proof/alethe/alethe_post_processor.cpp | 2 +- src/proof/alf/alf_printer.cpp | 2 +- src/smt/term_formula_removal.cpp | 4 ++-- src/theory/builtin/proof_checker.cpp | 4 ++-- 7 files changed, 11 insertions(+), 12 deletions(-) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index f377bd8ed2d..a0ed76fa929 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -336,14 +336,14 @@ enum ENUM(ProofRule) : uint32_t EVALUE(ANNOTATION), /** * \verbatim embed:rst:leading-asterisk - * **Processing rules -- Remove Term Formulas Axiom** + * **Processing rules -- If-then-else equivalence** * * .. math:: - * \inferrule{- \mid t}{\texttt{RemoveTermFormulas::getAxiomFor}(t)} + * \inferrule{- \mid \ite{C}{t_1}{t_2}}{\ite{C}{((\ite{C}{t_1}{t_2}) = t_1)}{((\ite{C}{t_1}{t_2}) = t_2)}} * * \endverbatim */ - EVALUE(REMOVE_TERM_FORMULA_AXIOM), + EVALUE(ITE_EQ), /** * \verbatim embed:rst:leading-asterisk diff --git a/proofs/alf/cvc5/rules/Builtin.smt3 b/proofs/alf/cvc5/rules/Builtin.smt3 index 618c881f315..8de9a65e334 100644 --- a/proofs/alf/cvc5/rules/Builtin.smt3 +++ b/proofs/alf/cvc5/rules/Builtin.smt3 @@ -46,7 +46,7 @@ :conclusion (run_process_scope F C) ) -(declare-rule remove_term_formula_axiom ((T Type) (b Bool) (t1 T) (t2 T)) +(declare-rule ite_eq ((T Type) (b Bool) (t1 T) (t2 T)) :args ((ite b t1 t2)) :conclusion (let ((k (ite b t1 t2))) (ite b (= k t1) (= k t2)))) diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index 9dcba613b32..35918ed37b9 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -38,8 +38,7 @@ const char* toString(ProofRule rule) case ProofRule::ANNOTATION: return "ANNOTATION"; case ProofRule::DSL_REWRITE: return "DSL_REWRITE"; case ProofRule::THEORY_REWRITE: return "THEORY_REWRITE"; - case ProofRule::REMOVE_TERM_FORMULA_AXIOM: - return "REMOVE_TERM_FORMULA_AXIOM"; + case ProofRule::ITE_EQ: return "ITE_EQ"; //================================================= Trusted rules case ProofRule::TRUST: return "TRUST"; case ProofRule::TRUST_THEORY_REWRITE: return "TRUST_THEORY_REWRITE"; diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 44a276c73e5..58c15667011 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -1272,7 +1272,7 @@ bool AletheProofPostprocessCallback::update(Node res, // For now this introduces a hole. The processing in the future should // generate corresponding Alethe steps for each particular axiom for term // removal (for example for the ITE case). - case ProofRule::REMOVE_TERM_FORMULA_AXIOM: + case ProofRule::ITE_EQ: { return addAletheStep(AletheRule::HOLE, res, diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 549a3dc1f2d..e114adf0726 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -135,7 +135,7 @@ bool AlfPrinter::isHandled(const ProofNode* pfn) const case ProofRule::STRING_LENGTH_NON_EMPTY: case ProofRule::RE_INTER: case ProofRule::RE_UNFOLD_POS: - case ProofRule::REMOVE_TERM_FORMULA_AXIOM: + case ProofRule::ITE_EQ: case ProofRule::INSTANTIATE: case ProofRule::SKOLEMIZE: case ProofRule::ALPHA_EQUIV: diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 3816290d28f..bc2551929be 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -318,7 +318,7 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, Trace("rtf-proof-debug") << "RemoveTermFormulas::run: justify " << newAssertion << " with ITE axiom" << std::endl; - // ---------------------- REMOVE_TERM_FORMULA_AXIOM + // ---------------------- ITE_EQ // (ite node[0] // (= node node[1]) ------------- MACRO_SR_PRED_INTRO // (= node node[2])) node = skolem @@ -328,7 +328,7 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, // Note that the MACRO_SR_PRED_INTRO step holds due to conversion // of skolem into its witness form, which is node. Node axiom = getAxiomFor(node); - d_lp->addStep(axiom, ProofRule::REMOVE_TERM_FORMULA_AXIOM, {}, {node}); + d_lp->addStep(axiom, ProofRule::ITE_EQ, {}, {node}); Node eq = node.eqNode(skolem); d_lp->addStep(eq, ProofRule::MACRO_SR_PRED_INTRO, {}, {eq}); d_lp->addStep(newAssertion, diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index dcde9e521b8..d52e0efa321 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -50,7 +50,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(ProofRule::EVALUATE, this); pc->registerChecker(ProofRule::ACI_NORM, this); pc->registerChecker(ProofRule::ANNOTATION, this); - pc->registerChecker(ProofRule::REMOVE_TERM_FORMULA_AXIOM, this); + pc->registerChecker(ProofRule::ITE_EQ, this); pc->registerChecker(ProofRule::ENCODE_PRED_TRANSFORM, this); pc->registerChecker(ProofRule::DSL_REWRITE, this); pc->registerChecker(ProofRule::THEORY_REWRITE, this); @@ -393,7 +393,7 @@ Node BuiltinProofRuleChecker::checkInternal(ProofRule id, } return args[0]; } - else if (id == ProofRule::REMOVE_TERM_FORMULA_AXIOM) + else if (id == ProofRule::ITE_EQ) { Assert(children.empty()); Assert(args.size() == 1);