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.

10 files changed, 26 insertions, 59 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());
diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index fc3f67cf0..2949cf105 100644
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -16,6 +16,7 @@
 #include "theory/arrays/inference_manager.h"
 
 #include "options/smt_options.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/theory.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
@@ -116,13 +117,15 @@ void InferenceManager::convert(PfRule& id,
       break;
     case PfRule::ARRAYS_EXT: children.push_back(exp); break;
     default:
-      if (id != PfRule::ARRAYS_TRUST)
+      if (id != PfRule::THEORY_INFERENCE)
       {
         Assert(false) << "Unknown rule " << id << "\n";
       }
       children.push_back(exp);
       args.push_back(conc);
-      id = PfRule::ARRAYS_TRUST;
+      args.push_back(
+          builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARRAYS));
+      id = PfRule::THEORY_INFERENCE;
       break;
   }
 }
diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp
index 6d546d746..557a43a02 100644
--- a/src/theory/arrays/proof_checker.cpp
+++ b/src/theory/arrays/proof_checker.cpp
@@ -31,8 +31,6 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
   pc->registerChecker(PfRule::ARRAYS_EXT, this);
   pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this);
-  // trusted rules
-  pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
 }
 
 Node ArraysProofRuleChecker::checkInternal(PfRule id,
@@ -111,13 +109,6 @@ Node ArraysProofRuleChecker::checkInternal(PfRule id,
     Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]);
     return args[0].eqNode(expandedEqRange);
   }
-  if (id == PfRule::ARRAYS_TRUST)
-  {
-    // "trusted" rules
-    Assert(!args.empty());
-    Assert(args[0].getType().isBoolean());
-    return args[0];
-  }
   // no rule
   return Node::null();
 }
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 1a6dfedbb..0f0d24cde 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1671,11 +1671,12 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     {
       preRegisterTermInternal(selConst);
     }
+    // not currently supported in proofs, use THEORY_INFERENCE
     d_im.assertInference(selConst.eqNode(defValue),
                          true,
                          InferenceId::ARRAYS_CONST_ARRAY_DEFAULT,
                          d_true,
-                         PfRule::ARRAYS_TRUST);
+                         PfRule::THEORY_INFERENCE);
   }
 
   const CTNodeList* stores = d_infoMap.getStores(a);
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index a4323a1d0..afbfd16c1 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -17,6 +17,7 @@
 
 #include "proof/proof.h"
 #include "proof/proof_checker.h"
+#include "theory/builtin/proof_checker.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/model_manager.h"
 #include "theory/rewriter.h"
@@ -243,7 +244,8 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
   {
     // failed to reconstruct, add trust
     Trace("dt-ipc") << "...failed " << infer << std::endl;
-    cdp->addStep(conc, PfRule::DT_TRUST, expv, {conc});
+    Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_DATATYPES);
+    cdp->addStep(conc, PfRule::THEORY_INFERENCE, expv, {conc, t});
   }
   else
   {
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 77f9a4c27..23ca26a1f 100644
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -30,8 +30,6 @@ void DatatypesProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::DT_COLLAPSE, this);
   pc->registerChecker(PfRule::DT_SPLIT, this);
   pc->registerChecker(PfRule::DT_CLASH, this);
-  // trusted rules
-  pc->registerTrustedChecker(PfRule::DT_TRUST, this, 2);
 }
 
 Node DatatypesProofRuleChecker::checkInternal(PfRule id,
@@ -122,12 +120,6 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id,
     }
     return nm->mkConst(false);
   }
-  else if (id == PfRule::DT_TRUST)
-  {
-    Assert(!args.empty());
-    Assert(args[0].getType().isBoolean());
-    return args[0];
-  }
   // no rule
   return Node::null();
 }
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index b8c0a851c..f48d29416 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -541,7 +541,7 @@ void InferProofCons::convert(InferenceId infer,
       if (conc.getKind() != OR)
       {
         // This should never happen. If it does, we resort to using
-        // STRING_TRUST below (in production mode).
+        // THEORY_INFERENCE below (in production mode).
         Assert(false) << "Expected OR conclusion for " << infer;
       }
       else
@@ -876,7 +876,7 @@ void InferProofCons::convert(InferenceId infer,
     case InferenceId::STRINGS_CTN_TRANS:
     case InferenceId::STRINGS_CTN_DECOMPOSE:
     default:
-      // do nothing, these will be converted to STRING_TRUST below since the
+      // do nothing, these will be converted to THEORY_INFERENCE below since the
       // rule is unknown.
       break;
   }
@@ -925,11 +925,14 @@ void InferProofCons::convert(InferenceId infer,
         Trace("strings-ipc-fail") << "    e: " << ec << std::endl;
       }
     }
-    // untrustworthy conversion, the argument of STRING_TRUST is its conclusion
+    // untrustworthy conversion, the argument of THEORY_INFERENCE is its
+    // conclusion
     ps.d_args.clear();
     ps.d_args.push_back(conc);
+    Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_STRINGS);
+    ps.d_args.push_back(t);
     // use the trust rule
-    ps.d_rule = PfRule::STRING_TRUST;
+    ps.d_rule = PfRule::THEORY_INFERENCE;
     // add to stats
     d_statistics.d_inferencesNoPf << infer;
   }
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 36b42f296..5a4008724 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -53,8 +53,6 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::RE_ELIM, this);
   pc->registerChecker(PfRule::STRING_CODE_INJ, this);
   pc->registerChecker(PfRule::STRING_SEQ_UNIT_INJ, this);
-  // trusted rules
-  pc->registerTrustedChecker(PfRule::STRING_TRUST, this, 2);
 }
 
 Node StringProofRuleChecker::checkInternal(PfRule id,
@@ -506,13 +504,6 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
     AlwaysAssert(t[0].getType() == t[1].getType());
     return t[0].eqNode(t[1]);
   }
-  else if (id == PfRule::STRING_TRUST)
-  {
-    // "trusted" rules
-    Assert(!args.empty());
-    Assert(args[0].getType().isBoolean());
-    return args[0];
-  }
   return Node::null();
 }