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

author	Morgan Deters <mdeters@gmail.com>
	Mon, 23 May 2011 21:58:12 +0000 (21:58 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Mon, 23 May 2011 21:58:12 +0000 (21:58 +0000)
commit	3f7f9df5f0c419b7f7dd39e32852161f406a441f
tree	67ae6454e4496f6370cf8236500946e2c7e926b0	tree
parent	91656937b2188f05cdd9b42955c04e6157349285	commit \| diff

Merge from arrays2 branch.

27 files changed:

src/expr/node.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arrays/Makefile.am		diff \| blob \| history
src/theory/arrays/array_info.cpp	[new file with mode: 0644]	blob
src/theory/arrays/array_info.h	[new file with mode: 0644]	blob
src/theory/arrays/kinds		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.h		diff \| blob \| history
src/theory/arrays/union_find.cpp	[new file with mode: 0644]	blob
src/theory/arrays/union_find.h	[new file with mode: 0644]	blob
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/backtrackable.h	[new file with mode: 0644]	blob
src/util/ntuple.h	[new file with mode: 0644]	blob
src/util/stats.h		diff \| blob \| history
src/util/triple.h	[deleted file]	blob \| history
test/Makefile.am		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/arrays/Makefile	[new file with mode: 0644]	blob
test/regress/regress0/arrays/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress0/arrays/arrays0.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arrays/arrays1.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arrays/arrays2.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arrays/arrays3.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arrays/arrays4.smt2	[new file with mode: 0644]	blob