projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f51491e) | patch
(proof-new) Add the term conversion sequence generator (#5097)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 30 Sep 2020 13:20:03 +0000 (08:20 -0500)
committerGitHub <noreply@github.com>
Wed, 30 Sep 2020 13:20:03 +0000 (08:20 -0500)
commit0cf0dc3b3661e668f8c03113faad5078d91cea98
tree78bd8ec763638e662d1f945d82f26607d2472793tree
parentf51491e43e86abb862ea081568b8aa106293d64acommit | diff
(proof-new) Add the term conversion sequence generator (#5097)

This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.
src/expr/CMakeLists.txt diff | blob | history
src/expr/proof_node_manager.cpp diff | blob | history
src/expr/proof_node_manager.h diff | blob | history
src/expr/tconv_seq_proof_generator.cpp [new file with mode: 0644] blob
src/expr/tconv_seq_proof_generator.h [new file with mode: 0644] blob