Uniform treatment of trusted theory inferences in proofs (#7044)

Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.

3 files changed, 9 insertions, 25 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index d8fc1c578..03db36bb5 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -29,6 +29,7 @@
 #include "theory/arith/congruence_manager.h"
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 
 using namespace std;
@@ -1820,9 +1821,11 @@ std::shared_ptr<ProofNode> Constraint::externalExplain(
         }
         case ArithProofType::IntHoleAP:
         {
-          pf = pnm->mkNode(PfRule::INT_TRUST,
+          Node t =
+              builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH);
+          pf = pnm->mkNode(PfRule::THEORY_INFERENCE,
                            children,
-                           {getProofLiteral()},
+                           {getProofLiteral(), t},
                            getProofLiteral());
           break;
         }
diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp
index 45f972038..0f4d97b4d 100644
--- a/src/theory/arith/pp_rewrite_eq.cpp
+++ b/src/theory/arith/pp_rewrite_eq.cpp
@@ -16,6 +16,7 @@
 #include "theory/arith/pp_rewrite_eq.h"
 
 #include "options/arith_options.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
@@ -44,10 +45,12 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom)
   // don't need to rewrite terms since rewritten is not a non-standard op
   if (proofsEnabled())
   {
+    Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH);
     return d_ppPfGen.mkTrustedRewrite(
         atom,
         rewritten,
-        d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
+        d_pnm->mkNode(
+            PfRule::THEORY_INFERENCE, {}, {atom.eqNode(rewritten), t}));
   }
   return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
 }
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
index 4e25ae76b..58de8e391 100644
--- a/src/theory/arith/proof_checker.cpp
+++ b/src/theory/arith/proof_checker.cpp
@@ -36,11 +36,8 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::INT_TIGHT_UB, this);
   pc->registerChecker(PfRule::INT_TIGHT_LB, this);
   pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this);
-
   pc->registerChecker(PfRule::ARITH_MULT_POS, this);
   pc->registerChecker(PfRule::ARITH_MULT_NEG, this);
-  // trusted rules
-  pc->registerTrustedChecker(PfRule::INT_TRUST, this, 2);
 }
 
 Node ArithProofRuleChecker::checkInternal(PfRule id,
@@ -340,25 +337,6 @@ Node ArithProofRuleChecker::checkInternal(PfRule id,
       }
       // Check that all have the same constant:
     }
-    case PfRule::INT_TRUST:
-    {
-      if (Debug.isOn("arith::pf::check::trust"))
-      {
-        Debug("arith::pf::check::trust") << "Arith PfRule:" << id << std::endl;
-        Debug("arith::pf::check::trust") << "  children: " << std::endl;
-        for (const auto& c : children)
-        {
-          Debug("arith::pf::check::trust") << "  * " << c << std::endl;
-        }
-        Debug("arith::pf::check::trust") << "  args:" << std::endl;
-        for (const auto& c : args)
-        {
-          Debug("arith::pf::check::trust") << "  * " << c << std::endl;
-        }
-      }
-      Assert(args.size() == 1);
-      return args[0];
-    }
     case PfRule::ARITH_OP_ELIM_AXIOM:
     {
       Assert(children.empty());