projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 81b7882) | patch
Added BitwiseEq bitvector rewrite
authorClark Barrett <barrett@cs.nyu.edu>
Wed, 30 May 2012 20:33:40 +0000 (20:33 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Wed, 30 May 2012 20:33:40 +0000 (20:33 +0000)
commit03305bfae27642ed714eab144cf977d1943bb88d
tree42e24296848e69a7c6d2f5dd3eed53b518dc1954tree
parent81b78827f65b42f22f16874bbf0c8269ed0734fccommit | diff
Added BitwiseEq bitvector rewrite
Added option "--repeat-simp" which repeats nonclausal simplification: 4 times,
twice before ite removal and twice after
Enabled these options (plus ite-simp) on QF_AUFBV, obtaining significant
speedup on dwp examples
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/theory_bv_rewriter.cpp diff | blob | history
src/util/options.cpp diff | blob | history
src/util/options.h diff | blob | history