projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a12827) | patch
Cegqi bv remove extract terms preprocess pass (#1376)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 21 Nov 2017 20:02:24 +0000 (14:02 -0600)
committerGitHub <noreply@github.com>
Tue, 21 Nov 2017 20:02:24 +0000 (14:02 -0600)
commit60f1dd27da89be80c172e15e01c49f58e0ceb6c0
treeb8aef41ea8e9e37d559b6309d7337109a7fd33aatree
parent4a12827561bc070fb5c7fd9baf1320a6bf154bc2commit | diff
Cegqi bv remove extract terms preprocess pass (#1376)

* Preprocess extract -> concat pass for cegqi bv.

* Add sygus bench

* Fixes, infrastructure.

* Minor fixes.

* Try

* Minor

* Minor

* Document

* Format

* Improving debug messages.

* Address

* Format

* Overlapping extracts.

* Format

* Minor

* Address review.

* Format

* Comment

* Format
src/options/quantifiers_options diff | blob | history
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/sygus/Base16_1.sy [new file with mode: 0644] blob
test/regress/regress0/sygus/Makefile.am diff | blob | history