diff options
author | Lachnitt <lachnitt@stanford.edu> | 2021-09-23 15:35:32 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-23 22:35:32 +0000 |
commit | 6b56848d3b09894aa4d987ca2e91a87ff1d022ab (patch) | |
tree | 3d1e9cdbc8afbc57d8e6ee347b6c69d4110a0d8b | |
parent | 1e9c3deaf16c1fefd7d8344b9e6b6ddb9a19756e (diff) |
[proofs[ Alethe: Fix Order of Arguments of addAletheStepFromOr (#7237)
Changes the order of the arguments of addAletheStepFromOr to be consistent with addAletheStep.
-rw-r--r-- | src/proof/alethe/alethe_post_processor.cpp | 2 | ||||
-rw-r--r-- | src/proof/alethe/alethe_post_processor.h | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp index 97afbdab0..6312f3140 100644 --- a/src/proof/alethe/alethe_post_processor.cpp +++ b/src/proof/alethe/alethe_post_processor.cpp @@ -444,8 +444,8 @@ bool AletheProofPostprocessCallback::addAletheStep( } bool AletheProofPostprocessCallback::addAletheStepFromOr( - Node res, AletheRule rule, + Node res, const std::vector<Node>& children, const std::vector<Node>& args, CDProof& cdp) diff --git a/src/proof/alethe/alethe_post_processor.h b/src/proof/alethe/alethe_post_processor.h index 4a7d8cf61..587190524 100644 --- a/src/proof/alethe/alethe_post_processor.h +++ b/src/proof/alethe/alethe_post_processor.h @@ -89,15 +89,15 @@ class AletheProofPostprocessCallback : public ProofNodeUpdaterCallback * This method internally calls addAletheStep. The kind of the given Node has * to be OR. * - * @param res The expected result of the application in form (or F1 ... Fn), * @param rule The id of the Alethe rule, + * @param res The expected result of the application in form (or F1 ... Fn), * @param children The children of the application, * @param args The arguments of the application * @param cdp The proof to add to * @return True if the step could be added, or false if not. */ - bool addAletheStepFromOr(Node res, - AletheRule rule, + bool addAletheStepFromOr(AletheRule rule, + Node res, const std::vector<Node>& children, const std::vector<Node>& args, CDProof& cdp); |