projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7d09d8b) | patch
Reorganizing initialization of term registry in quantifiers (#6127)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 15 Mar 2021 18:17:19 +0000 (13:17 -0500)
committerGitHub <noreply@github.com>
Mon, 15 Mar 2021 18:17:19 +0000 (18:17 +0000)
commit6d060743830ab21dc970444688fe1dc2ad34494f
treeee51b9642df2f12cec969a665472074c17e8457etree
parent7d09d8bffc4c055900ddf933db37355ec6258b06commit | diff
Reorganizing initialization of term registry in quantifiers (#6127)

This is in preparation for moving several utilities into the quantifiers inference manager.

This PR moves ownership of TermRegistry and QuantifiersRegistry to TheoryQuantifiers from QuantifiersEngine.
15 files changed:
src/theory/quantifiers/ematching/ho_trigger.cpp diff | blob | history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/ematching/trigger.cpp diff | blob | history
src/theory/quantifiers/relevant_domain.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.cpp diff | blob | history
src/theory/quantifiers/sygus/term_database_sygus.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers/term_registry.cpp diff | blob | history
src/theory/quantifiers/term_registry.h diff | blob | history
src/theory/quantifiers/term_tuple_enumerator.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history