git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 12 Aug 2020 05:08:32 +0000 (00:08 -0500)
committer	GitHub <noreply@github.com>
	Wed, 12 Aug 2020 05:08:32 +0000 (22:08 -0700)
commit	66836c5fd879c92bddbca52d4b1802213f227a44
tree	b0434cc3be08802a0028193ca91bda2c0e802af6	tree
parent	b5b2858807d48136807aba29bb53a1e91cfacc6e	commit \| diff

Split SmtEngineState from SmtEngine (#4855)

This splits a utility for tracking the "basic" state of the SmtEngine. This class tracks its high-level state, including the "SMT mode", last/expected status and manages the contexts. It is not responsible more detailed state information (e.g. the assertions).

21 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/api/cvc4cpp.cpp		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_engine_state.cpp	[new file with mode: 0644]	blob
src/smt/smt_engine_state.h	[new file with mode: 0644]	blob
src/smt/smt_mode.cpp	[new file with mode: 0644]	blob
src/smt/smt_mode.h	[new file with mode: 0644]	blob
test/unit/preprocessing/pass_bv_gauss_white.h		diff \| blob \| history
test/unit/prop/cnf_stream_white.h		diff \| blob \| history
test/unit/theory/evaluator_white.h		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.h		diff \| blob \| history
test/unit/theory/theory_arith_white.h		diff \| blob \| history
test/unit/theory/theory_bv_rewriter_white.h		diff \| blob \| history
test/unit/theory/theory_bv_white.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_instantiator_white.h		diff \| blob \| history
test/unit/theory/theory_sets_type_enumerator_white.h		diff \| blob \| history
test/unit/theory/theory_white.h		diff \| blob \| history
test/unit/theory/type_enumerator_white.h		diff \| blob \| history

RSS Atom