projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ba91b0e) | patch
Move decision manager into theory inference manager (#6231)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 29 Mar 2021 14:31:20 +0000 (09:31 -0500)
committerGitHub <noreply@github.com>
Mon, 29 Mar 2021 14:31:20 +0000 (14:31 +0000)
commit0e08fa4ff925b201d42544dd4b28c74d1b245bd7
tree60e6e3acb961cda82540903b834e27358f20bd99tree
parentba91b0ea10021ad299f30d23de4864940bb78100commit | diff
Move decision manager into theory inference manager (#6231)

This makes it so that the decision manager is accessible from TheoryInferenceManager.

This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.
22 files changed:
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/datatypes/sygus_extension.cpp diff | blob | history
src/theory/datatypes/sygus_extension.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.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/quantifiers_modules.cpp diff | blob | history
src/theory/quantifiers/quantifiers_modules.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_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/sep/theory_sep.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/theory.cpp diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_inference_manager.cpp diff | blob | history
src/theory/theory_inference_manager.h diff | blob | history
src/theory/uf/cardinality_extension.cpp diff | blob | history