Rename REMOVE_TERM_FORMULA_AXIOM to ITE_EQ (cvc5#10704)

Also makes the documentation explicitly given.
ajreynol · Apr 30, 2024 · c4f5de3 · c4f5de3
1 parent 92fa769
commit c4f5de3
Show file tree

Hide file tree

Showing 7 changed files with 11 additions and 12 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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);