Refactor trusted and macro proof rules (cvc5#10133)

This PR conglomerates a majority of our trusted proof rules into single rule ProofRule::TRUST for clarity, and introduces a subcategory TrustId that captures the source of the trusted step.

This allows us to simplify the API ProofRule enumeration.

It also does some minor renaming of macro proof rules (MACRO_ should be used for any rule that is not formally justifiable to external users but expected to be reconstructed internally).

include/cvc5/cvc5_proof_rule.h

@@ -156,7 +156,7 @@ enum ENUM(ProofRule) : uint32_t
    * where :math:`idr` is a MethodId identifier, which determines the kind of
    * rewriter to apply, e.g. Rewriter::rewrite. \endverbatim
    */
-  EVALUE(REWRITE),
+  EVALUE(MACRO_REWRITE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Builtin theory -- Evaluate**
@@ -315,17 +315,18 @@ enum ENUM(ProofRule) : uint32_t
 
   /**
    * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory lemma**
+   * **Trusted rule**
    *
    * .. math::
-   *   \inferrule{- \mid F, tid}{F}
+   *   \inferrule{F_1 \dots F_n \mid tid, F, ...}{F}
    *
-   * where :math:`F` is a (T-valid) theory lemma generated by theory with
-   * TheoryId :math:`tid`. This is a "coarse-grained" rule that is used as a
-   * placeholder if a theory did not provide a proof for a lemma or conflict.
+   * where :math:`tid` is an identifier and :math:`F` is a formula. This rule
+   * is used when a formal justification of an inference step cannot be provided.
+   * The formulas :math:`F_1 \dots F_n` refer to a set of formulas that
+   * entail :math:`F`, which may or may not be provided.
    * \endverbatim
    */
-  EVALUE(THEORY_LEMMA),
+  EVALUE(TRUST),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Trusted rules -- Theory rewrite**
@@ -343,146 +344,7 @@ enum ENUM(ProofRule) : uint32_t
    * bound variables that are not guaranteed to be consistent on each call.
    * \endverbatim
    */
-  EVALUE(THEORY_REWRITE),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory preprocessing**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t =
-   * \texttt{Theory::ppRewrite}(t)` for some theory. \endverbatim
-   */
-  EVALUE(THEORY_PREPROCESS),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory preprocessing**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` was added as a new assertion by theory preprocessing from
-   * the theory with identifier tid.
-   * \endverbatim
-   */
-  EVALUE(THEORY_PREPROCESS_LEMMA),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Preprocessing**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t = t'` where :math:`t`
-   * was replaced by :math:`t'` based on some preprocessing pass, or otherwise
-   * :math:`F` was added as a new assertion by some preprocessing pass.
-   * \endverbatim
-   */
-  EVALUE(PREPROCESS),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Preprocessing new assertion**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` was added as a new assertion by some preprocessing pass.
-   * \endverbatim
-   */
-  EVALUE(PREPROCESS_LEMMA),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Theory expand definitions**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t = t'` where :math:`t`
-   * was replaced by :math:`t'` based on theory expand definitions. \endverbatim
-   */
-  EVALUE(THEORY_EXPAND_DEF),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Witness term axiom**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an existential ``(exists ((x T)) (P x))`` used for
-   * introducing a witness term ``(witness ((x T)) (P x))``. \endverbatim
-   */
-  EVALUE(WITNESS_AXIOM),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-replayable rewriting**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality `t = t'` that holds by a form of rewriting
-   * that could not be replayed during proof postprocessing. \endverbatim
-   */
-  EVALUE(TRUST_REWRITE),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-supported flattening rewrite **
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality `t = t'` where both `t` and `t'` are
-   * applications of associative operators but the rewriter does not support
-   * flattening them to the same normal form. \endverbatim
-   */
-  EVALUE(TRUST_FLATTENING_REWRITE),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-replayable substitution**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality :math:`t = t'` that holds by a form of
-   * substitution that could not be replayed during proof postprocessing.
-   * \endverbatim
-   */
-  EVALUE(TRUST_SUBS),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Non-replayable substitution map**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is an equality :math:`t = t'` that holds by a form of
-   * substitution that could not be determined by the TrustSubstitutionMap. This
-   * inference may contain possibly multiple children corresponding to the
-   * formulas used to derive the substitution. \endverbatim
-   */
-  EVALUE(TRUST_SUBS_MAP),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Trusted rules -- Solved equality**
-   *
-   * .. math::
-   *   \inferrule{F' \mid F}{F}
-   *
-   * where :math:`F` is a solved equality of the form :math:`x = t` derived as
-   * the solved form of :math:`F'`. \endverbatim
-   */
-  EVALUE(TRUST_SUBS_EQ),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Theory-specific inference**
-   *
-   * .. math::
-   *   \inferrule{- \mid F}{F}
-   *
-   * where :math:`F` is a fact derived by a theory-specific inference.
-   * \endverbatim
-   */
-  EVALUE(THEORY_INFERENCE),
+  EVALUE(TRUST_THEORY_REWRITE),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **SAT Refutation for assumption-based unsat cores**
@@ -1276,7 +1138,7 @@ enum ENUM(ProofRule) : uint32_t
 
   /**
    * \verbatim embed:rst:leading-asterisk
-   * **Bit-vectors -- Bitblast**
+   * **Bit-vectors -- (Macro) Bitblast**
    *
    * .. math::
    *
@@ -1288,7 +1150,7 @@ enum ENUM(ProofRule) : uint32_t
    * strategies defined in ``theory/bv/bitblast/bitblast_strategies_template.h``.
    * \endverbatim
    */
-  EVALUE(BV_BITBLAST),
+  EVALUE(MACRO_BV_BITBLAST),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Bit-vectors -- Bitblast bit-vector constant, variable, and terms**
@@ -1459,19 +1321,6 @@ enum ENUM(ProofRule) : uint32_t
    * \endverbatim
    */
   EVALUE(ALPHA_EQUIV),
-  /**
-   * \verbatim embed:rst:leading-asterisk
-   * **Quantifiers -- (Trusted) quantifiers preprocessing**
-   *
-   * .. math::
-   *
-   *   \inferrule{?\mid F}{F}
-   *
-   * where :math:`F` is an equality of the form :math:`t =
-   * \texttt{QuantifiersPreprocess::preprocess(t)}`.
-   * \endverbatim
-   */
-  EVALUE(QUANTIFIERS_PREPROCESS),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Strings -- Core rules -- Concatenation equality**
@@ -1816,7 +1665,7 @@ enum ENUM(ProofRule) : uint32_t
   EVALUE(STRING_SEQ_UNIT_INJ),
   /**
    * \verbatim embed:rst:leading-asterisk
-   * **Strings -- (Trusted) String inference**
+   * **Strings -- (Macro) String inference**
    *
    * .. math::
    *
@@ -1826,7 +1675,7 @@ enum ENUM(ProofRule) : uint32_t
    * :math:`\texttt{strings::InferProofCons::convert}`.
    * \endverbatim
    */
-  EVALUE(STRING_INFERENCE),
+  EVALUE(MACRO_STRING_INFERENCE),
 
   /**
    * \verbatim embed:rst:leading-asterisk

src/CMakeLists.txt

@@ -212,6 +212,8 @@ libcvc5_add_sources(
   proof/proof_step_buffer.h
   proof/resolution_proofs_util.cpp
   proof/resolution_proofs_util.h
+  proof/trust_id.cpp
+  proof/trust_id.h
   proof/trust_node.cpp
   proof/trust_node.h
   proof/theory_proof_step_buffer.cpp

src/api/cpp/cvc5_proof_rule.cpp

@@ -27,7 +27,7 @@ const char* toString(ProofRule id)
     case ProofRule::ASSUME: return "ASSUME";
     case ProofRule::SCOPE: return "SCOPE";
     case ProofRule::SUBS: return "SUBS";
-    case ProofRule::REWRITE: return "REWRITE";
+    case ProofRule::MACRO_REWRITE: return "MACRO_REWRITE";
     case ProofRule::EVALUATE: return "EVALUATE";
     case ProofRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
     case ProofRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
@@ -38,20 +38,8 @@ const char* toString(ProofRule id)
     case ProofRule::DSL_REWRITE: return "DSL_REWRITE";
     case ProofRule::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
     //================================================= Trusted rules
-    case ProofRule::THEORY_LEMMA: return "THEORY_LEMMA";
-    case ProofRule::THEORY_REWRITE: return "THEORY_REWRITE";
-    case ProofRule::PREPROCESS: return "PREPROCESS";
-    case ProofRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
-    case ProofRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
-    case ProofRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA";
-    case ProofRule::THEORY_EXPAND_DEF: return "THEORY_EXPAND_DEF";
-    case ProofRule::WITNESS_AXIOM: return "WITNESS_AXIOM";
-    case ProofRule::TRUST_REWRITE: return "TRUST_REWRITE";
-    case ProofRule::TRUST_FLATTENING_REWRITE: return "TRUST_FLATTENING_REWRITE";
-    case ProofRule::TRUST_SUBS: return "TRUST_SUBS";
-    case ProofRule::TRUST_SUBS_MAP: return "TRUST_SUBS_MAP";
-    case ProofRule::TRUST_SUBS_EQ: return "TRUST_SUBS_EQ";
-    case ProofRule::THEORY_INFERENCE: return "THEORY_INFERENCE";
+    case ProofRule::TRUST: return "TRUST";
+    case ProofRule::TRUST_THEORY_REWRITE: return "TRUST_THEORY_REWRITE";
     case ProofRule::SAT_REFUTATION: return "SAT_REFUTATION";
     //================================================= Boolean rules
     case ProofRule::RESOLUTION: return "RESOLUTION";
@@ -126,7 +114,7 @@ const char* toString(ProofRule id)
     case ProofRule::ARRAYS_EXT: return "ARRAYS_EXT";
     case ProofRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND";
     //================================================= Bit-Vector rules
-    case ProofRule::BV_BITBLAST: return "BV_BITBLAST";
+    case ProofRule::MACRO_BV_BITBLAST: return "MACRO_BV_BITBLAST";
     case ProofRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP";
     case ProofRule::BV_EAGER_ATOM: return "BV_EAGER_ATOM";
     //================================================= Datatype rules
@@ -140,7 +128,6 @@ const char* toString(ProofRule id)
     case ProofRule::SKOLEMIZE: return "SKOLEMIZE";
     case ProofRule::INSTANTIATE: return "INSTANTIATE";
     case ProofRule::ALPHA_EQUIV: return "ALPHA_EQUIV";
-    case ProofRule::QUANTIFIERS_PREPROCESS: return "QUANTIFIERS_PREPROCESS";
     //================================================= String rules
     case ProofRule::CONCAT_EQ: return "CONCAT_EQ";
     case ProofRule::CONCAT_UNIFY: return "CONCAT_UNIFY";
@@ -162,7 +149,7 @@ const char* toString(ProofRule id)
     case ProofRule::RE_ELIM: return "RE_ELIM";
     case ProofRule::STRING_CODE_INJ: return "STRING_CODE_INJ";
     case ProofRule::STRING_SEQ_UNIT_INJ: return "STRING_SEQ_UNIT_INJ";
-    case ProofRule::STRING_INFERENCE: return "STRING_INFERENCE";
+    case ProofRule::MACRO_STRING_INFERENCE: return "MACRO_STRING_INFERENCE";
     //================================================= Arith rules
     case ProofRule::MACRO_ARITH_SCALE_SUM_UB: return "MACRO_ARITH_SCALE_SUM_UB";
     case ProofRule::ARITH_SUM_UB: return "ARITH_SUM_UB";

src/preprocessing/assertion_pipeline.cpp

@@ -197,7 +197,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
       //   rewrite( d_nodes[i] ^ n )
       // allocate a fresh proof which will act as the proof generator
       LazyCDProof* lcp = d_pppg->allocateHelperProof();
-      lcp->addLazyStep(n, pg, ProofRule::PREPROCESS);
+      lcp->addLazyStep(n, pg, TrustId::PREPROCESS);
       // if newConj was constructed by AND above, use AND_INTRO
       if (newConj != n)
       {

src/preprocessing/passes/non_clausal_simp.cpp

@@ -121,12 +121,12 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   // constant propagations
   std::shared_ptr<TrustSubstitutionMap> constantPropagations =
       std::make_shared<TrustSubstitutionMap>(
-          d_env, u, "NonClausalSimp::cprop", ProofRule::PREPROCESS_LEMMA);
+          d_env, u, "NonClausalSimp::cprop", TrustId::PREPROCESS_LEMMA);
   SubstitutionMap& cps = constantPropagations->get();
   // new substitutions
   std::shared_ptr<TrustSubstitutionMap> newSubstitutions =
       std::make_shared<TrustSubstitutionMap>(
-          d_env, u, "NonClausalSimp::newSubs", ProofRule::PREPROCESS_LEMMA);
+          d_env, u, "NonClausalSimp::newSubs", TrustId::PREPROCESS_LEMMA);
   SubstitutionMap& nss = newSubstitutions->get();
 
   size_t j = 0;

src/proof/alethe/alethe_post_processor.cpp

@@ -383,7 +383,7 @@ bool AletheProofPostprocessCallback::update(Node res,
 
       return success;
     }
-    case ProofRule::THEORY_REWRITE:
+    case ProofRule::TRUST_THEORY_REWRITE:
     {
       return addAletheStep(AletheRule::ALL_SIMPLIFY,
                            res,

src/proof/conv_proof_generator.cpp

@@ -75,7 +75,7 @@ void TConvProofGenerator::addRewriteStep(Node t,
                                          Node s,
                                          ProofGenerator* pg,
                                          bool isPre,
-                                         ProofRule trustId,
+                                         TrustId trustId,
                                          bool isClosed,
                                          uint32_t tctx)
 {

src/proof/conv_proof_generator.h

@@ -158,7 +158,7 @@ class TConvProofGenerator : protected EnvObj, public ProofGenerator
                       Node s,
                       ProofGenerator* pg,
                       bool isPre = false,
-                      ProofRule trustId = ProofRule::ASSUME,
+                      TrustId trustId = TrustId::NONE,
                       bool isClosed = false,
                       uint32_t tctx = 0);
   /** Same as above, for a single step */