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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 25 Aug 2021 16:27:03 +0000 (11:27 -0500)
committer	GitHub <noreply@github.com>
	Wed, 25 Aug 2021 16:27:03 +0000 (16:27 +0000)
commit	76c8bc4c963b494db36074afac74e51ab39917e4
tree	1dead31654b75eec05ada6ca0a4adf2878809cab	tree
parent	9a4deadddfd3d4489ba15f65f0e3dab72b2fcccc	commit \| diff

Eliminate calls to currentSmtEngine (#7060)

Work towards supporting multiple solvers running in parallel.

There are now only 5 remaining internal calls to smt::currentSmtEngine.

More will be eliminated on future PRs.

35 files changed:

src/preprocessing/passes/sort_infer.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.h		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.h		diff \| blob \| history
src/theory/quantifiers/expr_miner_manager.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner_manager.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator.h		diff \| blob \| history
src/theory/quantifiers/solution_filter.cpp		diff \| blob \| history
src/theory/quantifiers/solution_filter.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.h		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.h		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_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.h		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history

RSS Atom