projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 36d01a7) | patch
[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 13 Jul 2021 18:38:23 +0000 (15:38 -0300)
committerGitHub <noreply@github.com>
Tue, 13 Jul 2021 18:38:23 +0000 (13:38 -0500)
commit912be5c60f194c3b0d52c1d06a1339fb6cb13a9c
treed82fa967ecf45342133369c8641aac02ca633016tree
parent36d01a7fd74c6dff52bf9dcba490ff7ded29ad5dcommit | diff
[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)

Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.
src/prop/sat_proof_manager.cpp diff | blob | history
src/theory/booleans/theory_bool_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 [new file with mode: 0644] blob