projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bb816ef) | patch
[proofs] [alethe] Introduce all_simplify and replace old trust rules (#8100)
authorLachnitt <lachnitt@stanford.edu>
Thu, 17 Feb 2022 18:08:46 +0000 (10:08 -0800)
committerGitHub <noreply@github.com>
Thu, 17 Feb 2022 18:08:46 +0000 (18:08 +0000)
commite97f9447ed646d4a15ba1c107fa8a0f94165353b
treed38f12a917cd0aea36eba0b53d3841250b57862btree
parentbb816ef2cb29aaacda9d5f21d15b6fb120a64b19commit | diff
[proofs] [alethe] Introduce all_simplify and replace old trust rules (#8100)

Instead of printing "trust" in the case of a simplification rule that cannot be translated to an Alethe simplify rule print "all_simplify". This also replaces the heuristic in THEORY_REWRITE to determine which simplify rule is needed.
src/proof/alethe/alethe_post_processor.cpp diff | blob | history
src/proof/alethe/alethe_proof_rule.cpp diff | blob | history
src/proof/alethe/alethe_proof_rule.h diff | blob | history