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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 30 Nov 2020 16:56:28 +0000 (10:56 -0600)
committer	GitHub <noreply@github.com>
	Mon, 30 Nov 2020 16:56:28 +0000 (10:56 -0600)
commit	9f372f084f5c558e3ff618d02abfdb384a82e066
tree	eebab887048231876505ced878b5b7878ffb72b6	tree
parent	ac6150d7992b5dd1cace8d8d6e0d308e4a741c12	commit \| diff

Remove includes for old API from internal code (#5536)

The only code including the old API now are in parser/ and main/ which will require further untangling.

23 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/array.h	[deleted file]	blob \| history
src/expr/symbol_table.h		diff \| blob \| history
src/expr/type.h		diff \| blob \| history
src/expr/type_properties_template.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/dump_manager.cpp		diff \| blob \| history
src/smt/listeners.cpp		diff \| blob \| history
src/smt/model_blocker.h		diff \| blob \| history
src/smt/model_core_builder.h		diff \| blob \| history
src/smt/proof_manager.h		diff \| blob \| history
src/smt_util/boolean_simplification.h		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/quantifiers/expr_miner.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_qe_preproc.h		diff \| blob \| history
src/theory/smt_engine_subsolver.h		diff \| blob \| history

RSS Atom