projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4ee85fb) | patch
Add simple inferences for extended bitvector functions, add a few related options...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 11 Nov 2016 18:59:13 +0000 (12:59 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 11 Nov 2016 19:07:55 +0000 (13:07 -0600)
commite2f28f39b3a3749a5eeed5294f25bec1e210b129
tree6bd5fc8c198139bdf518ad3ae443d87eac13816ftree
parent4ee85fbbe8f1bbc6261b804916f897b26d500fbfcommit | diff
Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.
src/options/bv_options diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
test/regress/regress0/bv/Makefile.am diff | blob | history
test/regress/regress0/bv/bv-int-collapse1.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv-int-collapse2-sat.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv-int-collapse2.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv2nat-simp-range.smt2 [new file with mode: 0644] blob