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

author	Liana Hadarean <lianahady@gmail.com>
	Thu, 22 Mar 2012 21:45:31 +0000 (21:45 +0000)
committer	Liana Hadarean <lianahady@gmail.com>
	Thu, 22 Mar 2012 21:45:31 +0000 (21:45 +0000)
commit	c0324db3ac7e5984c632f46690f58c333b9a42b2
tree	7a9a83b7dc1f929d4eb3de06b59ed6ff7b7f43bd	tree
parent	8c4495b18e40a406be35baceaf473878bcc375f1	commit \| diff

Merged updated version of the bitvector theory:
* added simplification rewrites

23 files changed:

src/prop/bvminisat/core/Solver.cc		diff \| blob \| history
src/prop/sat_module.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/bv/Makefile.am		diff \| blob \| history
src/theory/bv/bitblast_strategies.cpp		diff \| blob \| history
src/theory/bv/bitblast_strategies.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_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_arith.h	[deleted file]	blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h	[new file with mode: 0644]	blob
src/theory/bv/theory_bv_rewrite_rules_core.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h	[new file with mode: 0644]	blob
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h	[new file with mode: 0644]	blob
src/theory/bv/theory_bv_rewrite_rules_simplification.h	[new file with mode: 0644]	blob
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
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history