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.

diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 008b0dc6f45f40dd6275ff60b19ebd789f36a33b..286396523db4aad3dd8d8c0c2e3d1a17f6f7e9c3 100644 (file)
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -79,7 +79,6 @@ const char* toString(PfRule id)
     case PfRule::ITE_ELIM2: return "ITE_ELIM2";
     case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1";
     case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2";
-    //================================================= De Morgan rules
     case PfRule::NOT_AND: return "NOT_AND";
     //================================================= CNF rules
     case PfRule::CNF_AND_POS: return "CNF_AND_POS";
@@ -120,7 +119,6 @@ const char* toString(PfRule id)
       return "ARRAYS_READ_OVER_WRITE_CONTRA";
     case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
     case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
-    case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
     case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND";
     //================================================= Bit-Vector rules
     case PfRule::BV_BITBLAST: return "BV_BITBLAST";
@@ -132,7 +130,6 @@ const char* toString(PfRule id)
     case PfRule::DT_COLLAPSE: return "DT_COLLAPSE";
     case PfRule::DT_SPLIT: return "DT_SPLIT";
     case PfRule::DT_CLASH: return "DT_CLASH";
-    case PfRule::DT_TRUST: return "DT_TRUST";
     //================================================= Quantifiers rules
     case PfRule::SKOLEM_INTRO: return "SKOLEM_INTRO";
     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
@@ -160,7 +157,6 @@ const char* toString(PfRule id)
     case PfRule::RE_ELIM: return "RE_ELIM";
     case PfRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
     case PfRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
-    case PfRule::STRING_TRUST: return "STRING_TRUST";
     //================================================= Arith rules
     case PfRule::MACRO_ARITH_SCALE_SUM_UB:
       return "ARITH_SCALE_SUM_UPPER_BOUNDS";
@@ -168,7 +164,6 @@ const char* toString(PfRule id)
     case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
     case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
     case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
-    case PfRule::INT_TRUST: return "INT_TRUST";
     case PfRule::ARITH_MULT_SIGN: return "ARITH_MULT_SIGN";
     case PfRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
     case PfRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 78e773bdc4d1f492b1449d69bd4c6850b33cd7fb..7a3ce6882df4e78147bb3da309d36b3dba208e77 100644 (file)
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -722,12 +722,6 @@ enum class PfRule : uint32_t
   //              (forall ((x T))
   //               (=> (and (<= i x) (<= x j)) (= (select a x) (select b x)))))
   ARRAYS_EQ_RANGE_EXPAND,
-  // ======== Array Trust
-  // Children: (P1 ... Pn)
-  // Arguments: (F)
-  // ---------------------
-  // Conclusion: F
-  ARRAYS_TRUST,
 
   //================================================= Bit-Vector rules
   // Note: bitblast() represents the result of the bit-blasted term as a
@@ -800,12 +794,6 @@ enum class PfRule : uint32_t
   // Conclusion: false
   // for i != j.
   DT_CLASH,
-  // ======== Datatype Trust
-  // Children: (P1 ... Pn)
-  // Arguments: (F)
-  // ---------------------
-  // Conclusion: F
-  DT_TRUST,
 
   //================================================= Quantifiers rules
   // ======== Skolem intro
@@ -1082,12 +1070,6 @@ enum class PfRule : uint32_t
   // Also applies to the case where (seq.unit y) is a constant sequence
   // of length one.
   STRING_SEQ_UNIT_INJ,
-  // ======== String Trust
-  // Children: none
-  // Arguments: (Q)
-  // ---------------------
-  // Conclusion: (Q)
-  STRING_TRUST,
 
   //================================================= Arithmetic rules
   // ======== Adding Inequalities
@@ -1152,12 +1134,6 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: arith::OperatorElim::getAxiomFor(t)
   ARITH_OP_ELIM_AXIOM,
-  // ======== Int Trust
-  // Children: (P1 ... Pn)
-  // Arguments: (Q)
-  // ---------------------
-  // Conclusion: (Q)
-  INT_TRUST,
 
   //======== Multiplication sign inference
   // Children: none

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index d8fc1c57808ec3225606734b3fe9cceebadbf26b..03db36bb554a3a31a39a422684345e964a4e49f7 100644 (file)
--- 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 45f972038320dd7dc40dacfb828c5c4f2dbce5ee..0f4d97b4d058731ebfbd7791b01bf59e8698d01a 100644 (file)
--- 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 4e25ae76ba0d00b0d1936af30220fad76fde84b3..58de8e391e7d6be24e1ff6294b05d4a74ba8fc20 100644 (file)
--- 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 fc3f67cf047569ff8adbd4a4b673a86ec62c6a9a..2949cf1057e404b6e9b8a80fd401bb225bc46b1c 100644 (file)
--- 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 6d546d7461306c3a8796d700a38b293a47f167a9..557a43a028350640cda9c1cd55b568736ff5c1be 100644 (file)
--- 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 1a6dfedbbdd09d52a4057cf0b0d5d5305cd5c5c0..0f0d24cde869fbd2bb3f131716fa82609d2e7830 100644 (file)
--- 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 a4323a1d0317820593a41cf2000014ce6a8801fe..afbfd16c14a65e2eb3e653183b5f12c5da299800 100644 (file)
--- 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 77f9a4c2794d33445cfc7c2bab257392a80cf87c..23ca26a1fba4bfea38d40faec73fe9c8a76e8d32 100644 (file)
--- 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 b8c0a851ccadec257f0481c5b6785db34830877e..f48d2941628b966bf95ac8b53ed2e44f72fe1a3c 100644 (file)
--- 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 36b42f29648c395b83bfc70d39614041646147e9..5a4008724f1794ff7519d1a787dbf7d81107160a 100644 (file)
--- 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();
 }