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

author	Gereon Kremer <nafur42@gmail.com>
	Mon, 16 Aug 2021 14:20:22 +0000 (07:20 -0700)
committer	GitHub <noreply@github.com>
	Mon, 16 Aug 2021 14:20:22 +0000 (14:20 +0000)
commit	5e31ee3a34388d6d44129e898897bdb1297009de
tree	b12a86a3737c23555444d2ed6c5c3f13b737b7a4	tree
parent	0711ec521f01888b059d152d1c1f20382d5ce432	commit \| diff

Make Theory class use Env (#7011)

This PR changes the Theory base class and the constructors of all theories to use the Env class to access contexts, logic information and the proof node manager.

35 files changed:

src/smt/env.cpp		diff \| blob \| history
src/smt/env.h		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/bags/theory_bags.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.h		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history
test/unit/theory/theory_white.cpp		diff \| blob \| history

RSS Atom