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

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Mon, 20 Sep 2010 01:08:32 +0000 (01:08 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Mon, 20 Sep 2010 01:08:32 +0000 (01:08 +0000)
commit	1b30b256a0ec40ff431b83296bfe5aa0e099eb2e
tree	91fb063e9cfcf360d601e21a19996995576ece7d	tree
parent	9eaf94708275337a4749b7ef2f44bf1c6746d8fc	commit \| diff

bitvector rewriting for the core theory and testcases

85 files changed:

src/expr/node_builder.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/parser/antlr_input.h		diff \| blob \| history
src/parser/smt/Smt.g		diff \| blob \| history
src/parser/smt/smt.cpp		diff \| blob \| history
src/theory/bv/Makefile.am		diff \| blob \| history
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/theory_bv.cpp	[new file with mode: 0644]	blob
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.cpp	[new file with mode: 0644]	blob
src/theory/bv/theory_bv_rewrite_rules.h	[new file with mode: 0644]	blob
src/theory/bv/theory_bv_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h	[new file with mode: 0644]	blob
src/util/bitvector.h		diff \| blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
test/regress/regress0/bv/core/concat-merge-0.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/concat-merge-0.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/concat-merge-1.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/concat-merge-1.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/concat-merge-2.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/concat-merge-2.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/concat-merge-3.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/concat-merge-3.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-0.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-0.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-1.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-1.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-10.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-10.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-11.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-11.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-2.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-2.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-3.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-3.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-4.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-4.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-5.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-5.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-6.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-6.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-7.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-7.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-8.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-8.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-9.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-concat-9.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-constant.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-constant.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-0.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-0.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-1.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-1.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-10.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-10.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-11.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-11.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-2.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-2.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-3.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-3.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-4.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-4.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-5.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-5.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-6.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-6.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-7.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-7.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-8.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-8.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-9.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-extract-9.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-0.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-0.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-1.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-1.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-2.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-2.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-3.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-3.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-4.cvc	[new file with mode: 0644]	blob
test/regress/regress0/bv/core/extract-whole-4.smt	[new file with mode: 0644]	blob

RSS Atom