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

author	Liana Hadarean <lianahady@gmail.com>
	Wed, 4 Apr 2012 02:02:06 +0000 (02:02 +0000)
committer	Liana Hadarean <lianahady@gmail.com>
	Wed, 4 Apr 2012 02:02:06 +0000 (02:02 +0000)
commit	52d6dc20c61007a5c066590aa1fd0b95ed3c2527
tree	040efec36cde7775b5c19eb43fcdd60cbeb61f9e	tree
parent	4fa8c7d1a0654e7780fd485c51463c06b34379b5	commit \| diff

   * added propagation as lemmas to TheoryBV:
   * modified BVMinisat to work incrementally
   * added more bv regressions

40 files changed:

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/core/SolverTypes.h		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.h		diff \| blob \| history
src/prop/cryptominisat/MTRand/Makefile.in		diff \| blob \| history
src/prop/cryptominisat/Makefile.in		diff \| blob \| history
src/prop/cryptominisat/Solver/Makefile.in		diff \| blob \| history
src/prop/cryptominisat/man/Makefile.in		diff \| blob \| history
src/prop/cryptominisat/mtl/Makefile.in		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_factory.h		diff \| blob \| history
src/theory/bv/bitblast_strategies.cpp		diff \| blob \| history
src/theory/bv/bv_sat.cpp		diff \| blob \| history
src/theory/bv/bv_sat.h		diff \| blob \| history
src/theory/bv/kinds		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.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_core.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
test/regress/regress0/bv/fuzz01.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz02.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz03.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz04.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz05.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz06.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz07.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz08.smt	[new file with mode: 0644]	blob
test/regress/regress0/bv/fuzz09.smt	[new file with mode: 0644]	blob

RSS Atom