git.libre-soc.org Git - cvc5.git/commit

author	ajreynol <andrew.j.reynolds@gmail.com>
	Thu, 13 Oct 2016 22:44:19 +0000 (17:44 -0500)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Thu, 13 Oct 2016 22:44:19 +0000 (17:44 -0500)
commit	9da056f71c0c4a8ed5afd01c300e9c86cfcf5601
tree	9cc4ed5a09640c3dbb8df9cbaf242ade0f8acc4f	tree
parent	7e750757ac9832b70b5c6ca1d15e17cddbd2e6c0	commit \| diff

Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.

21 files changed:

src/theory/bv/aig_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.h		diff \| blob \| history
src/theory/bv/bv_subtheory_inequality.cpp		diff \| blob \| history
src/theory/bv/eager_bitblaster.cpp		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/lazy_bitblaster.cpp		diff \| blob \| history
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_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
test/regress/regress0/bv/bv2nat-ground-c.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bv/bv2nat-ground.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bv/cmu-rdk-3.smt2	[new file with mode: 0644]	blob