summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorLachnitt <lachnitt@stanford.edu>2021-09-23 15:35:32 -0700
committerGitHub <noreply@github.com>2021-09-23 22:35:32 +0000
commit6b56848d3b09894aa4d987ca2e91a87ff1d022ab (patch)
tree3d1e9cdbc8afbc57d8e6ee347b6c69d4110a0d8b
parent1e9c3deaf16c1fefd7d8344b9e6b6ddb9a19756e (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.cpp2
-rw-r--r--src/proof/alethe/alethe_post_processor.h6
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback