projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9760607) | patch
Clean Ceg Instantiators (#1365)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 14 Nov 2017 19:42:48 +0000 (13:42 -0600)
committerGitHub <noreply@github.com>
Tue, 14 Nov 2017 19:42:48 +0000 (13:42 -0600)
commit376d72fd02d7f8822188055355452449b718481f
tree51606e49c6d140edb07688fb3f0b707dc1b6ae7atree
parent976060724c9059db511714fd5f135897768a112ecommit | diff
Clean Ceg Instantiators (#1365)

* Initial setup for preprocessing counterexample lemmas.

* Improve documentation.

* Improving documentation, infrastructure.

* Extraction -> concatentation as a preprocess step.

* Clang format

* Minor

* Make option, refactor effort levels.

* Format

* Clean

* Format

* Rename

* Format

* More

* Format

* Splitting changes.

* Format

* Revert option.

* Minor

* Format
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_instantiator.h diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.cpp diff | blob | history
src/theory/quantifiers/ceg_t_instantiator.h diff | blob | history
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/extract-nproc.smt2 [new file with mode: 0644] blob