projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ef31c25) | patch
Miscellaneous elimination of dependencies on quantifiers engine (#6238)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 30 Mar 2021 00:52:48 +0000 (19:52 -0500)
committerGitHub <noreply@github.com>
Tue, 30 Mar 2021 00:52:48 +0000 (00:52 +0000)
commit7e5fe049ad88405a90fd5a43caa872d646d4b8e2
tree2fe225b29e2721c8d5237f0628e2a393a001bc99tree
parentef31c2518c194029a913fe2872e2040d2f5e4294commit | diff
Miscellaneous elimination of dependencies on quantifiers engine  (#6238)

This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
12 files changed:
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/cegqi/ceg_instantiator.h diff | blob | history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp diff | blob | history
src/theory/quantifiers/ematching/im_generator.h diff | blob | history
src/theory/quantifiers/quantifiers_modules.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/sygus_process_conj.h diff | blob | history
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_qe_preproc.h diff | blob | history
src/theory/quantifiers/sygus/synth_engine.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history