projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1cb1934) | patch
Remove dependencies on smt engine in smt solver (#6965)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 4 Aug 2021 01:15:43 +0000 (20:15 -0500)
committerGitHub <noreply@github.com>
Wed, 4 Aug 2021 01:15:43 +0000 (20:15 -0500)
commit19c382b8666492fa8818444c7f2ee907da3d9479
tree4521883b52170aa1d7ac5fadbf29b5bb0f26f087tree
parent1cb1934d76f25e9f42f51b2eead733b3e9e12236commit | diff
Remove dependencies on smt engine in smt solver (#6965)

This is work towards eliminating circular dependencies on SmtEngine.

This simplifies several interfaces and makes it so that SmtSolver does not take a pointer to its parent SmtEngine.

It is also work towards eliminating the output manager, which is now subsumed by Env.
src/prop/cnf_stream.cpp diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_solver.cpp diff | blob | history
src/smt/smt_solver.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
test/unit/prop/cnf_stream_white.cpp diff | blob | history