projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 31b3986) | patch
Minor cleanup of quantifiers engine (#4994)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 3 Sep 2020 21:00:26 +0000 (16:00 -0500)
committerGitHub <noreply@github.com>
Thu, 3 Sep 2020 21:00:26 +0000 (16:00 -0500)
commit8828e545cfb838d806a0ad382671a9af131e8431
treea488c085adf0ba36b2d3a0d24b547c1a2eb29926tree
parent31b3986ea297d54e828cd6c34e3689435ba63d7ccommit | diff
Minor cleanup of quantifiers engine (#4994)

Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs.
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp 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_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history