projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 704fd54) | patch
Remove `TheoryState::options()` (#7148)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 9 Sep 2021 01:28:25 +0000 (18:28 -0700)
committerGitHub <noreply@github.com>
Thu, 9 Sep 2021 01:28:25 +0000 (01:28 +0000)
commitdfd135ee8039c901e535b0781ae1b27cb3365166
treeeaaae51ad04de4b3d66d006d5f30e8e3a469ff93tree
parent704fd545440023a0deaa328a9de9c11ac5fe963ccommit | diff
Remove `TheoryState::options()` (#7148)

This commit removes TheoryState::options() by changing more classes to
EnvObjs.
53 files changed:
src/theory/arith/arith_preprocess.cpp diff | blob | history
src/theory/arith/arith_preprocess.h diff | blob | history
src/theory/arith/branch_and_bound.cpp diff | blob | history
src/theory/arith/branch_and_bound.h diff | blob | history
src/theory/arith/equality_solver.cpp diff | blob | history
src/theory/arith/equality_solver.h diff | blob | history
src/theory/arith/inference_manager.cpp diff | blob | history
src/theory/arith/nl/iand_solver.cpp diff | blob | history
src/theory/arith/nl/iand_solver.h diff | blob | history
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/pow2_solver.cpp diff | blob | history
src/theory/arith/nl/pow2_solver.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arrays/inference_manager.cpp diff | blob | history
src/theory/bags/term_registry.cpp diff | blob | history
src/theory/bags/term_registry.h diff | blob | history
src/theory/bags/theory_bags.cpp diff | blob | history
src/theory/datatypes/inference_manager.cpp diff | blob | history
src/theory/datatypes/sygus_extension.cpp diff | blob | history
src/theory/quantifiers/ematching/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/ematching/instantiation_engine.h diff | blob | history
src/theory/quantifiers/equality_query.cpp diff | blob | history
src/theory/quantifiers/equality_query.h diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/first_order_model.h diff | blob | history
src/theory/quantifiers/fmf/first_order_model_fmc.cpp diff | blob | history
src/theory/quantifiers/fmf/first_order_model_fmc.h diff | blob | history
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/quantifiers/fmf/full_model_check.h diff | blob | history
src/theory/quantifiers/fmf/model_builder.cpp diff | blob | history
src/theory/quantifiers/fmf/model_builder.h diff | blob | history
src/theory/quantifiers/ho_term_database.cpp diff | blob | history
src/theory/quantifiers/ho_term_database.h diff | blob | history
src/theory/quantifiers/instantiate.cpp diff | blob | history
src/theory/quantifiers/instantiate.h diff | blob | history
src/theory/quantifiers/quant_relevance.cpp diff | blob | history
src/theory/quantifiers/quant_relevance.h diff | blob | history
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/quantifiers_inference_manager.cpp diff | blob | history
src/theory/quantifiers/quantifiers_modules.cpp diff | blob | history
src/theory/quantifiers/quantifiers_registry.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.h diff | blob | history
src/theory/quantifiers/sygus/enum_value_manager.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_conjecture.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/term_pools.cpp diff | blob | history
src/theory/quantifiers/term_pools.h diff | blob | history
src/theory/quantifiers/term_registry.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/theory_state.h diff | blob | history