projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e5bbc45) | patch
Remove more static option accesses (#7582)
authorGereon Kremer <nafur42@gmail.com>
Tue, 9 Nov 2021 01:00:35 +0000 (17:00 -0800)
committerGitHub <noreply@github.com>
Tue, 9 Nov 2021 01:00:35 +0000 (01:00 +0000)
commit932c33baa92bd45377b872eaec91b2c7721ff916
treea463df3492b25c2d22acaa823f4640c988d9ddb3tree
parente5bbc45d20caf51e7df8288d51f20eb12da72abacommit | diff
Remove more static option accesses (#7582)

This PR removes more than half of the remaining static option accesses options::foo() from the theory solvers.
40 files changed:
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/fmf/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/quantifiers/fmf/model_builder.cpp diff | blob | history
src/theory/quantifiers/fun_def_evaluator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_enumerative.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_pool.cpp diff | blob | history
src/theory/quantifiers/quant_split.cpp diff | blob | history
src/theory/quantifiers/quantifiers_registry.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/skolemize.cpp diff | blob | history
src/theory/quantifiers/solution_filter.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_unif.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_interpol.h diff | blob | history
src/theory/quantifiers/sygus/sygus_pbe.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_repair_const.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_unif_io.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp diff | blob | history
src/theory/quantifiers/sygus/synth_engine.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/sygus_inst.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/theory_quantifiers.cpp diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/regexp_solver.cpp diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/uf/cardinality_extension.cpp diff | blob | history
src/theory/uf/cardinality_extension.h diff | blob | history
src/theory/uf/ho_extension.cpp diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history