projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8287028) | patch
Make CnfStream::toCNF iterative (#6757)
authorMathias Preiner <mathias.preiner@gmail.com>
Fri, 18 Jun 2021 17:31:53 +0000 (10:31 -0700)
committerGitHub <noreply@github.com>
Fri, 18 Jun 2021 17:31:53 +0000 (17:31 +0000)
commit5b15ba18c32ed78190b7e71b6bfb64f1f8b8dcab
tree2c27fbe335ba1fd42c452511c1955b2339b53974tree
parent828702825ab82175029e087eb8911575acd43a82commit | diff
Make CnfStream::toCNF iterative (#6757)

This commit makes toCNF() iterative to avoid this issue.
Note that the order in which nodes are visited and thus SatLiterals are
created remains the same.

Fixes #6111
src/prop/cnf_stream.cpp diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/proof_cnf_stream.h diff | blob | history
test/api/CMakeLists.txt diff | blob | history
test/api/issue6111.cpp [new file with mode: 0644] blob