[proof-new] Updating documentation for Subs/Rw ids (#6502)

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 432ff1f899f69f8ae935255a7bb35832da0fe73d..4730df652571ea5bf44378ef5b3fba234328d28a 100644 (file)
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -106,19 +106,19 @@ enum class PfRule : uint32_t
   // rewritten form under a (proven) substitution.
   //
   // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (t, (ids (idr)?)?)
+  // Arguments: (t, (ids (ida (idr)?)?)?)
   // ---------------------------------------------------------------
   // Conclusion: (= t t')
   // where
   //   t' is
-  //   Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  //   Rewriter{idr}(t*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
   //
   // In other words, from the point of view of Skolem forms, this rule
   // transforms t to t' by standard substitution + rewriting.
   //
-  // The argument ids and idr is optional and specify the identifier of the
-  // substitution and rewriter respectively to be used. For details, see
-  // theory/builtin/proof_checker.h.
+  // The arguments ids, ida and idr are optional and specify the identifier of
+  // the substitution, the substitution application and rewriter respectively to
+  // be used. For details, see theory/builtin/proof_checker.h.
   MACRO_SR_EQ_INTRO,
   // ======== Substitution + Rewriting predicate introduction
   //
@@ -126,11 +126,11 @@ enum class PfRule : uint32_t
   // that it rewrites to true under a proven substitution.
   //
   // Children: (P1:F1, ..., Pn:Fn)
-  // Arguments: (F, (ids (idr)?)?)
+  // Arguments: (F, (ids (ida (idr)?)?)?)
   // ---------------------------------------------------------------
   // Conclusion: F
   // where
-  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true
+  //   Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) == true
   // where ids and idr are method identifiers.
   //
   // More generally, this rule also holds when:
@@ -152,12 +152,12 @@ enum class PfRule : uint32_t
   // rewritten form under a proven substitution.
   //
   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
-  // Arguments: ((ids (idr)?)?)
+  // Arguments: ((ids (ida (idr)?)?)?)
   // ----------------------------------------
   // Conclusion: F'
   // where
   //   F' is
-  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)).
+  //   Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)).
   // where ids and idr are method identifiers.
   //
   // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO.
@@ -169,12 +169,12 @@ enum class PfRule : uint32_t
   // substitution.
   //
   // Children: (P1:F, P2:F1, ..., P_{n+1}:Fn)
-  // Arguments: (G, (ids (idr)?)?)
+  // Arguments: (G, (ids (ida (idr)?)?)?)
   // ----------------------------------------
   // Conclusion: G
   // where
-  //   Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) ==
-  //   Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1))
+  //   Rewriter{idr}(F*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1)) ==
+  //   Rewriter{idr}(G*sigma{ids, ida}(Fn)*...*sigma{ids, ida}(F1))
   //
   // More generally, this rule also holds when:
   //   Rewriter::rewrite(toOriginal(F')) == Rewriter::rewrite(toOriginal(G'))

diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index fdc952bdd0a7d6362833dd3a4bf1dcf3639e739f..9dfc9418f77b17de09ebfa34f0356db2ecfd3c43 100644 (file)
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -481,6 +481,8 @@ bool BuiltinProofRuleChecker::getMethodIds(const std::vector<Node>& args,
       break;
     }
   }
+  Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / "
+                           << ida << " / " << idr << "\n";
   return true;
 }
 

diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 81da0a9695dc90458a31e6d11fe525eafc9c897a..dd6bf82e7faf1796622938eb824f11e9d48dc201 100644 (file)
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -137,6 +137,9 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * is derived from
    * @param ids The method identifier of the substitution, by default SB_DEFAULT
    * specifying that lhs/rhs of equalities are interpreted as a substitution.
+   * @param ida The method identifier of the substitution application, by
+   * default SB_SEQUENTIAL specifying that substitutions are to be applied
+   * sequentially
    * @return The substituted form of n.
    */
   static Node applySubstitution(Node n,
@@ -154,6 +157,7 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
    * @param n The node to substitute and rewrite,
    * @param exp The (set of) equalities corresponding to the substitution
    * @param ids The method identifier of the substitution.
+   * @param ida The method identifier of the substitution application.
    * @param idr The method identifier of the rewriter.
    * @return The substituted, rewritten form of n.
    */
@@ -166,8 +170,8 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
   static bool getMethodId(TNode n, MethodId& i);
   /**
    * Get method identifiers from args starting at the given index. Store their
-   * values into ids, idr. This method returns false if args does not contain
-   * valid method identifiers at position index in args.
+   * values into ids, ida, and idr. This method returns false if args does not
+   * contain valid method identifiers at position index in args.
    */
   bool getMethodIds(const std::vector<Node>& args,
                     MethodId& ids,
@@ -175,8 +179,8 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
                     MethodId& idr,
                     size_t index);
   /**
-   * Add method identifiers ids and idr as nodes to args. This does not add ids
-   * or idr if their values are the default ones.
+   * Add method identifiers ids, ida and idr as nodes to args. This does not add
+   * ids, ida or idr if their values are the default ones.
    */
   static void addMethodIds(std::vector<Node>& args,
                            MethodId ids,