projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 21f9e53) | patch
Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV
authorClark Barrett <barrett@cs.nyu.edu>
Mon, 28 May 2012 16:27:50 +0000 (16:27 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Mon, 28 May 2012 16:27:50 +0000 (16:27 +0000)
commit5c61887222630583b48bd26fc914d166f122c252
tree7d3027303409ad803cb1771195ec7cbd90f9f984tree
parent21f9e53792ba5f94594fccb7bef880aa77b266cbcommit | diff
Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV
17 files changed:
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/bv/bitblast_strategies.cpp 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_operator_elimination.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_utils.h diff | blob | history
src/theory/ite_simplifier.cpp diff | blob | history
src/theory/ite_simplifier.h diff | blob | history
src/theory/rewriter.cpp diff | blob | history
src/theory/rewriter.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history