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

author	Andres Noetzli <andres.noetzli@gmail.com>
	Mon, 29 Jun 2020 22:35:44 +0000 (15:35 -0700)
committer	GitHub <noreply@github.com>
	Mon, 29 Jun 2020 22:35:44 +0000 (17:35 -0500)
commit	19054b3b1d427e662d30d4322df2b2f2361353da
tree	1ee878fd6c2c36b78ea33607a5668e6a6d8f7144	tree
parent	5cd6f0e5e910ad61ebc5045170842078818a3b80	commit \| diff

Make ExprManager constructor private (#4669)

This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.

30 files changed:

examples/CMakeLists.txt		diff \| blob \| history
examples/api/java/CMakeLists.txt		diff \| blob \| history
examples/simple_vc_cxx.cpp		diff \| blob \| history
examples/simple_vc_quant_cxx.cpp		diff \| blob \| history
src/expr/expr_manager_template.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.h		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/smt_engine_subsolver.cpp		diff \| blob \| history
src/theory/smt_engine_subsolver.h		diff \| blob \| history
test/system/CMakeLists.txt		diff \| blob \| history
test/system/boilerplate.cpp		diff \| blob \| history
test/system/reset_assertions.cpp		diff \| blob \| history
test/system/statistics.cpp		diff \| blob \| history
test/system/two_smt_engines.cpp	[deleted file]	blob \| history
test/system/two_solvers.cpp	[new file with mode: 0644]	blob
test/unit/expr/attribute_black.h		diff \| blob \| history
test/unit/expr/expr_manager_public.h		diff \| blob \| history
test/unit/expr/expr_public.h		diff \| blob \| history
test/unit/expr/symbol_table_black.h		diff \| blob \| history
test/unit/expr/type_cardinality_public.h		diff \| blob \| history
test/unit/theory/regexp_operation_black.h		diff \| blob \| history
test/unit/theory/theory_black.h		diff \| blob \| history
test/unit/util/array_store_all_black.h		diff \| blob \| history
test/unit/util/datatype_black.h		diff \| blob \| history

RSS Atom