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

author	lianah <lianahady@gmail.com>
	Tue, 10 Jun 2014 17:48:45 +0000 (13:48 -0400)
committer	lianah <lianahady@gmail.com>
	Tue, 10 Jun 2014 17:48:45 +0000 (13:48 -0400)
commit	5f072a19d299191dbedc4b69c8e0eda694cfa957
tree	0ebfc27bd05d06b0cdb2fc0813b7d5649d36aee4	tree
parent	db51926b5ce806754fc26c81b1b7d3e739fc4fc5	commit \| diff

Merging CAV14 paper bit-vector work.

63 files changed:

configure.ac		diff \| blob \| history
contrib/run-script-smtcomp2014		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/main/command_executor_portfolio.cpp		diff \| blob \| history
src/main/portfolio.cpp		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/cnf_stream.cpp		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_factory.h		diff \| blob \| history
src/smt/options_handlers.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/bv/abstraction.cpp	[new file with mode: 0644]	blob
src/theory/bv/abstraction.h	[new file with mode: 0644]	blob
src/theory/bv/aig_bitblaster.h	[new file with mode: 0644]	blob
src/theory/bv/bitblast_mode.cpp	[new file with mode: 0644]	blob
src/theory/bv/bitblast_mode.h	[new file with mode: 0644]	blob
src/theory/bv/bitblast_strategies.cpp	[deleted file]	blob \| history
src/theory/bv/bitblast_strategies.h	[deleted file]	blob \| history
src/theory/bv/bitblast_strategies_template.h	[new file with mode: 0644]	blob
src/theory/bv/bitblast_utils.h	[new file with mode: 0644]	blob
src/theory/bv/bitblaster.cpp	[deleted file]	blob \| history
src/theory/bv/bitblaster.h	[deleted file]	blob \| history
src/theory/bv/bitblaster_template.h	[new file with mode: 0644]	blob
src/theory/bv/bv_eager_solver.cpp	[new file with mode: 0644]	blob
src/theory/bv/bv_eager_solver.h	[new file with mode: 0644]	blob
src/theory/bv/bv_quick_check.cpp	[new file with mode: 0644]	blob
src/theory/bv/bv_quick_check.h	[new file with mode: 0644]	blob
src/theory/bv/bv_subtheory.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp	[new file with mode: 0644]	blob
src/theory/bv/bv_subtheory_algebraic.h	[new file with mode: 0644]	blob
src/theory/bv/bv_subtheory_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_bitblast.h		diff \| blob \| history
src/theory/bv/bv_subtheory_core.cpp		diff \| blob \| history
src/theory/bv/bv_subtheory_core.h		diff \| blob \| history
src/theory/bv/bv_to_bool.cpp		diff \| blob \| history
src/theory/bv/bv_to_bool.h		diff \| blob \| history
src/theory/bv/eager_bitblaster.h	[new file with mode: 0644]	blob
src/theory/bv/kinds		diff \| blob \| history
src/theory/bv/lazy_bitblaster.h	[new file with mode: 0644]	blob
src/theory/bv/options		diff \| blob \| history
src/theory/bv/options_handlers.h	[new file with mode: 0644]	blob
src/theory/bv/slicer.cpp		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_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_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp	[new file with mode: 0644]	blob
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/unconstrained_simplifier.cpp		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
test/regress/regress0/bv/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/divtest.smt2	[new file with mode: 0644]	blob

RSS Atom