projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 89b6c05) | patch
Add Gaussian Elimination as a preprocessing pass for BV. (#1342)
authorAina Niemetz <aina.niemetz@gmail.com>
Thu, 30 Nov 2017 23:50:00 +0000 (15:50 -0800)
committerGitHub <noreply@github.com>
Thu, 30 Nov 2017 23:50:00 +0000 (15:50 -0800)
commit4c1f1cad720a94226f7834874cf59478de35b74a
treeb97655661092e2597b31c089ec9bc52e77d33ec9tree
parent89b6c052e96cc907800650de93d2f238e19acd38commit | diff
Add Gaussian Elimination as a preprocessing pass for BV. (#1342)

This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.
src/Makefile.am diff | blob | history
src/options/bv_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/bvgauss.cpp [new file with mode: 0644] blob
src/theory/bv/bvgauss.h [new file with mode: 0644] blob
test/unit/Makefile.am diff | blob | history
test/unit/theory/theory_bv_bvgauss_white.h [new file with mode: 0644] blob