projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bb0fc30) | patch
basic union find for bitvectors
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Fri, 24 Sep 2010 15:03:28 +0000 (15:03 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Fri, 24 Sep 2010 15:03:28 +0000 (15:03 +0000)
commit353c6d5c3770365f0dffcbdf697199bed156cf50
treee8a019cf24b3a4dd2b4eb458cbe066164b6eddeetree
parentbb0fc300c810f68f1e901413272c6658e31d60f9commit | diff
basic union find for bitvectors
27 files changed:
src/theory/bv/Makefile.am diff | blob | history
src/theory/bv/equality_engine.cpp [new file with mode: 0644] blob
src/theory/bv/equality_engine.h [new file with mode: 0644] blob
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
src/theory/bv/theory_bv_rewrite_rules.cpp diff | blob | history
src/theory/bv/theory_bv_rewrite_rules.h diff | blob | history
src/theory/bv/theory_bv_utils.h diff | blob | history
src/theory/theory_engine.h diff | blob | history
test/regress/regress0/bv/core/Makefile.am diff | blob | history
test/regress/regress0/bv/core/bv_eq_diamond10.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/bv_eq_diamond11.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/bv_eq_diamond12.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/bv_eq_diamond13.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/bv_eq_diamond14.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/bv_eq_diamond15.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/bv_eq_diamond16.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/bv_eq_diamond17.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-00.cvc [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-00.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-01.cvc [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-01.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-02.cvc [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-02.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-03.cvc [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-03.smt [new file with mode: 0644] blob
test/regress/regress0/bv/core/equality-04.smt [new file with mode: 0644] blob