[alethe] Add arguments to rules and/not_or/and_pos/or_neg (cvc5#11123)

HanielB · Aug 9, 2024 · 0b00421 · 0b00421
1 parent 5a8bfb5
commit 0b00421
Showing 1 changed file with 12 additions and 4 deletions.
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
@@ -774,7 +774,7 @@ bool AletheProofPostprocessCallback::update(Node res,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           {},
+                           args,
                            *cdp);
     }
     // ======== And introduction
@@ -826,7 +826,7 @@ bool AletheProofPostprocessCallback::update(Node res,
                            res,
                            nm->mkNode(Kind::SEXPR, d_cl, res),
                            children,
-                           {},
+                           args,
                            *cdp);
     }
     // ======== Implication elimination
@@ -921,7 +921,11 @@ bool AletheProofPostprocessCallback::update(Node res,
     // The following rules are all translated according to the clause pattern.
     case ProofRule::CNF_AND_POS:
     {
-      return addAletheStepFromOr(AletheRule::AND_POS, res, children, {}, *cdp);
+      return addAletheStepFromOr(AletheRule::AND_POS,
+                                 res,
+                                 children,
+                                 std::vector<Node>{args.back()},
+                                 *cdp);
     }
     case ProofRule::CNF_AND_NEG:
     {
@@ -933,7 +937,11 @@ bool AletheProofPostprocessCallback::update(Node res,
     }
     case ProofRule::CNF_OR_NEG:
     {
-      return addAletheStepFromOr(AletheRule::OR_NEG, res, children, {}, *cdp);
+      return addAletheStepFromOr(AletheRule::OR_NEG,
+                                 res,
+                                 children,
+                                 std::vector<Node>{args.back()},
+                                 *cdp);
     }
     case ProofRule::CNF_IMPLIES_POS:
     {