projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b5073e1) | patch
Introduce quantifiers term registry (#5983)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 2 Mar 2021 03:37:03 +0000 (21:37 -0600)
committerGitHub <noreply@github.com>
Tue, 2 Mar 2021 03:37:03 +0000 (03:37 +0000)
commit4132e91fdb2f8912a89a101e96c86bf5076b327a
tree9d773b3a36aa68bda3d7b7839d9d8cd72a4061eftree
parentb5073e16ea49ce9214fcc5318ce080724719c809commit | diff
Introduce quantifiers term registry (#5983)

This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
src/CMakeLists.txt diff | blob | history
src/theory/quantifiers/equality_query.cpp diff | blob | history
src/theory/quantifiers/equality_query.h 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_registry.cpp [new file with mode: 0644] blob
src/theory/quantifiers/term_registry.h [new file with mode: 0644] blob
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history