projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c884127) | patch
Initial working version of BV word-level instantiation (#1158)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 29 Sep 2017 12:23:22 +0000 (07:23 -0500)
committerGitHub <noreply@github.com>
Fri, 29 Sep 2017 12:23:22 +0000 (07:23 -0500)
commit8011f2715fa6ba312fd766cab5249648598310d4
tree97dd3469f470510d810a8f4191c470b9209539a6tree
parentc884127d6d3cc3444a18ec8a9fb9a5096ae482b0commit | diff
Initial working version of BV word-level instantiation (#1158)

* Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems.

* Guard by option, minor notes.

* Minor

* Minor fixes.

* Minor
src/options/quantifiers_options 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/qbv-simple-2vars-vo.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 [new file with mode: 0644] blob