diff options
| -rw-r--r-- | src/expr/proof_rule.h | 24 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 2 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.h | 12 |
3 files changed, 22 insertions, 16 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 432ff1f89..4730df652 100644 --- 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 fdc952bdd..9dfc9418f 100644 --- 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 81da0a969..dd6bf82e7 100644 --- 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, |