projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2f78ed8) | patch
Eliminate more circular dependencies on solver engine (#7311)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 7 Oct 2021 01:16:20 +0000 (20:16 -0500)
committerGitHub <noreply@github.com>
Thu, 7 Oct 2021 01:16:20 +0000 (01:16 +0000)
commit838a04edc3a41c98ee3a8121d4687e987f559fd1
treef6bdd6cbee636c87621bdf7e5ecb00d68a185b91tree
parent2f78ed85a8263d7ad632e679034e662091511670commit | diff
Eliminate more circular dependencies on solver engine (#7311)

This is work towards replacing our old dump infrastructure. This PR also does some initial reorganization towards printing assertions using the print benchmark utility.
20 files changed:
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/prop/prop_proof_manager.cpp diff | blob | history
src/prop/prop_proof_manager.h diff | blob | history
src/smt/assertions.cpp diff | blob | history
src/smt/assertions.h diff | blob | history
src/smt/check_models.cpp diff | blob | history
src/smt/check_models.h diff | blob | history
src/smt/preprocessor.cpp diff | blob | history
src/smt/preprocessor.h diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/process_assertions.h diff | blob | history
src/smt/proof_manager.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/smt/smt_solver.cpp diff | blob | history
src/smt/smt_solver.h diff | blob | history
src/smt/solver_engine.cpp diff | blob | history
src/smt/sygus_solver.cpp diff | blob | history
src/smt/sygus_solver.h diff | blob | history
src/smt/unsat_core_manager.cpp diff | blob | history