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

author	Liana Hadarean <lianahady@gmail.com>
	Tue, 8 May 2012 21:54:55 +0000 (21:54 +0000)
committer	Liana Hadarean <lianahady@gmail.com>
	Tue, 8 May 2012 21:54:55 +0000 (21:54 +0000)
commit	8a0c0562cb8d0e26ea019ff782b25c1997a49a0b
tree	28239db9bcb26b03d893ad61dd1a7ea099391fbe	tree
parent	5082cb8349efbb287084293cd4bc6c3fa5a34f26	commit \| diff

Merging in bvprop branch, with proper bit-vector propagation.
This should also fix bug 325.

33 files changed:

.project		diff \| blob \| history
.settings/net.certiv.antlrdt.core.prefs		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/prop/bvminisat/core/Solver.h		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/theory/bv/bv_sat.cpp		diff \| blob \| history
src/theory/bv/bv_sat.h		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_utils.h		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/util/node_visitor.h		diff \| blob \| history
src/util/options.cpp		diff \| blob \| history
src/util/options.h		diff \| blob \| history
test/regress/regress0/aufbv/fuzz00.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/fuzz10.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz11.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz12.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz13.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz14.smt	[new file with mode: 0644]	blob
test/unit/theory/theory_bv_white.h		diff \| blob \| history

RSS Atom