projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4b580ea) | patch
(Move-only) Split quant util (#1306)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 2 Nov 2017 04:20:09 +0000 (23:20 -0500)
committerGitHub <noreply@github.com>
Thu, 2 Nov 2017 04:20:09 +0000 (23:20 -0500)
commit3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9
treeb5c785e9a5e16d430f45b2a40f78e40247111233tree
parent4b580ea3876055f701b13e67e0e4e78abbe47674commit | diff
(Move-only) Split quant util (#1306)

* Initial draft of splitting quant util.

* Minor

* Document recursive term builder.

* Rename file, minor.

* Clang format
15 files changed:
src/Makefile.am diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_e_matching.cpp diff | blob | history
src/theory/quantifiers/quant_epr.cpp [new file with mode: 0644] blob
src/theory/quantifiers/quant_epr.h [new file with mode: 0644] blob
src/theory/quantifiers/quant_relevance.cpp [new file with mode: 0644] blob
src/theory/quantifiers/quant_relevance.h [new file with mode: 0644] blob
src/theory/quantifiers/quant_util.cpp diff | blob | history
src/theory/quantifiers/quant_util.h diff | blob | history
src/theory/quantifiers/sygus_explain.cpp [new file with mode: 0644] blob
src/theory/quantifiers/sygus_explain.h [new file with mode: 0644] blob
src/theory/quantifiers/term_database_sygus.h 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