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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 26 Nov 2020 05:03:11 +0000 (23:03 -0600)
committer	GitHub <noreply@github.com>
	Thu, 26 Nov 2020 05:03:11 +0000 (23:03 -0600)
commit	c41a2e9be2422a211b9687833c97ba37485cd946
tree	6e7f88a41d6bbb2581762de203f66086fe16ed49	tree
parent	d0c352ec04846353d630073e78e5b2fea92133c2	commit \| diff

Fully decouple SmtEngine and the Expr layer (#5532)

This removes the remaining dependencies of SmtEngine on the Expr layer. It now takes a NodeManager instead of a ExprManager.

27 files changed:

src/api/cvc4cpp.cpp		diff \| blob \| history
src/expr/type.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/smt_engine_subsolver.cpp		diff \| blob \| history
test/unit/expr/attribute_white.h		diff \| blob \| history
test/unit/expr/type_node_white.h		diff \| blob \| history
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_bags_normal_form_white.h		diff \| blob \| history
test/unit/theory/theory_bags_rewriter_white.h		diff \| blob \| history
test/unit/theory/theory_bags_type_rules_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_quantifiers_bv_inverter_white.h		diff \| blob \| history
test/unit/theory/theory_sets_type_enumerator_white.h		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.h		diff \| blob \| history
test/unit/theory/theory_strings_skolem_cache_black.h		diff \| blob \| history
test/unit/theory/theory_strings_word_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