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

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Wed, 6 Jun 2012 06:12:40 +0000 (06:12 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Wed, 6 Jun 2012 06:12:40 +0000 (06:12 +0000)
commit	fd9e22c4a2e57c3dfeda4de3842a3fb3ca4776ba
tree	047e4d27f725e9157ed5bef5357d0d72560218ae	tree
parent	2799ae1cf57ed2b98387a1de1325bccd89bd2a30	commit \| diff

Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5

38 files changed:

src/expr/kind_template.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/bv/bv_subtheory_eq.cpp		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_test_utils.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/equality_engine_types.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/util/options.cpp		diff \| blob \| history
test/regress/regress0/aufbv/Makefile	[new file with mode: 0644]	blob
test/regress/regress0/aufbv/Makefile.am		diff \| blob \| history
test/regress/regress0/aufbv/no_init_multi_delete14.smt	[new file with mode: 0644]	blob
test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt	[new file with mode: 0644]	blob
test/regress/regress0/aufbv/wchains010ue.delta01.smt	[new file with mode: 0644]	blob
test/regress/regress0/aufbv/wchains010ue.delta02.smt	[new file with mode: 0644]	blob
test/regress/regress0/aufbv/wchains010ue.smt	[new file with mode: 0644]	blob
test/regress/regress0/auflia/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/bug345.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt	[new file with mode: 0644]	blob
test/regress/regress0/uflia/Makefile.am		diff \| blob \| history
test/regress/regress0/uflia/error0.delta01.smt	[new file with mode: 0644]	blob
test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt	[new file with mode: 0644]	blob
test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt	[new file with mode: 0644]	blob
test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt	[new file with mode: 0644]	blob
test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt	[new file with mode: 0644]	blob
test/system/boilerplate.cpp		diff \| blob \| history
test/unit/theory/theory_black.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history

RSS Atom