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

author	Andres Noetzli <andres.noetzli@gmail.com>
	Thu, 9 Sep 2021 18:37:49 +0000 (11:37 -0700)
committer	GitHub <noreply@github.com>
	Thu, 9 Sep 2021 18:37:49 +0000 (18:37 +0000)
commit	e5aaebbbc5ea11b0cb3468169e5c80bf38868c82
tree	b422de3845c5c316b174d0ebff4835d0dad75f0d	tree
parent	08d770f84c3959c076cc693de9e251e910e508a7	commit \| diff

Remove `TheoryState::getEnv()` (#7163)

38 files changed:

src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_pool.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_pool.h		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quant_module.cpp		diff \| blob \| history
src/theory/quantifiers/quant_module.h		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.h		diff \| blob \| history
src/theory/quantifiers/term_registry.cpp		diff \| blob \| history
src/theory/quantifiers/term_registry.h		diff \| blob \| history
src/theory/theory_state.h		diff \| blob \| history

RSS Atom