Alethe: Add function that adds final steps to proof (#7710)
authorLachnitt <lachnitt@stanford.edu>
Wed, 1 Dec 2021 02:46:26 +0000 (18:46 -0800)
committerGitHub <noreply@github.com>
Wed, 1 Dec 2021 02:46:26 +0000 (02:46 +0000)
commitcd7d8ce26f5d4a5864b1dce78473c97a51394e40
tree6834cc7b3286410cc0d51bdd487a8be4f7df373e
parent24663f1c4baa2d60f27bd72c5654eaab9bd7ce01
Alethe: Add function that adds final steps to proof (#7710)

There are some cases when the result has to be transformed, e.g. when it was printed as (cl false) which is correct everywhere except in the last step. This function then transforms the result into (cl).

Should be merged after PR #7675.

Co-authored-by: Haniel Barbosa hanielbbarbosa@gmail.com
src/proof/alethe/alethe_post_processor.cpp
src/proof/alethe/alethe_post_processor.h