projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ddf6526) | patch
Split SmtSolver from SmtEngine (#4880)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 13 Aug 2020 20:22:59 +0000 (15:22 -0500)
committerGitHub <noreply@github.com>
Thu, 13 Aug 2020 20:22:59 +0000 (15:22 -0500)
commit02fa1dea5a8335a6bd5a1f3e8718796a9489ac8e
treecc6573fb7ae6bc9d70345788df445940d9f1aabetree
parentddf6526f9f3ac2410849fbf8ebf0eac09ff2a28acommit | diff
Split SmtSolver from SmtEngine (#4880)

This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.

This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).
src/CMakeLists.txt diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/smt/smt_solver.cpp [new file with mode: 0644] blob
src/smt/smt_solver.h [new file with mode: 0644] blob
test/unit/theory/theory_arith_white.h diff | blob | history
test/unit/theory/theory_bv_white.h diff | blob | history
test/unit/theory/theory_white.h diff | blob | history