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

author	Andres Noetzli <andres.noetzli@gmail.com>
	Mon, 13 Sep 2021 23:14:54 +0000 (16:14 -0700)
committer	GitHub <noreply@github.com>
	Mon, 13 Sep 2021 23:14:54 +0000 (18:14 -0500)
commit	a37f486c6e10b882a81474418e1d3f4ffdbd583c
tree	6b73a761684a5caba5745c7e5fbc37102beccebd	tree
parent	09cbf1c5746c69854a7578263240101e2430173e	commit \| diff

Remove context getters from `TheoryState` (#7174)

This removes TheoryState::getSatContext() and
TheoryState::getUserContext().

61 files changed:

src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/bv/bv_solver.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast_internal.h		diff \| blob \| history
src/theory/bv/bv_solver_layered.cpp		diff \| blob \| history
src/theory/bv/bv_solver_layered.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.h		diff \| blob \| history
src/theory/decision_strategy.cpp		diff \| blob \| history
src/theory/decision_strategy.h		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		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/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_inference_manager.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.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_registry.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.h		diff \| blob \| history
src/theory/sets/term_registry.cpp		diff \| blob \| history
src/theory/sets/term_registry.h		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.h		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/base_solver.h		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.h		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/extf_solver.h		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.h		diff \| blob \| history
src/theory/strings/strings_fmf.cpp		diff \| blob \| history
src/theory/strings/strings_fmf.h		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/term_registry.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/theory_state.cpp		diff \| blob \| history
src/theory/theory_state.h		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/ho_extension.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history

RSS Atom