Skip to content

Commit

Permalink
start removing custom assume
Browse files Browse the repository at this point in the history
  • Loading branch information
HanielB committed Feb 16, 2024
1 parent e348165 commit 3809b90
Showing 1 changed file with 2 additions and 7 deletions.
9 changes: 2 additions & 7 deletions src/proof/alethe/alethe_post_processor.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,6 @@ bool AletheProofPostprocessCallback::update(Node res,
case ProofRule::ASSUME:
{
return false;
// return addAletheStep(AletheRule::ASSUME, res, res, children, {}, *cdp);
}
// See proof_rule.h for documentation on the SCOPE rule. This comment uses
// variable names as introduced there. Since the SCOPE rule originally
Expand Down Expand Up @@ -2058,12 +2057,8 @@ bool AletheProofPostprocessCallback::maybeReplacePremiseProof(Node premise,
// step will be present in cdp connecting premiseChildConclusion to
// premiseChildPf (since by default adding an ASSUME step will not rewrite an
// existing proof for a node).
addAletheStep(AletheRule::ASSUME,
premiseChildConclusion,
premiseChildConclusion,
{},
{},
*cdp);
cdp->addStep(
premiseChildConclusion, ProofRule::ASSUME, {}, {premiseChildConclusion});
// equate it to what we expect, use equiv elim and resolution to
// obtain a proof the expected
Node equiv = premiseChildConclusion.eqNode(premise);
Expand Down

0 comments on commit 3809b90

Please sign in to comment.