projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5181426) | patch
Added some ITE rewrites,
authorClark Barrett <barrett@cs.nyu.edu>
Fri, 11 May 2012 14:00:27 +0000 (14:00 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Fri, 11 May 2012 14:00:27 +0000 (14:00 +0000)
commit57790a14676596e8c6ed42ff7ecd8038ddbaf09b
tree7e4d5c81f197beab924092fb72cc945d48a47e69tree
parent5181426cd8def23d67b69227fff033ef12850e68commit | diff
Added some ITE rewrites,
Added ITE simplifier - on by default only for QF_LIA benchmarks
Fixed one bug in arrays
Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()
13 files changed:
src/expr/node.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/Makefile.am diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/booleans/theory_bool_rewriter.cpp diff | blob | history
src/theory/ite_simplifier.cpp [new file with mode: 0644] blob
src/theory/ite_simplifier.h [new file with mode: 0644] blob
src/theory/shared_terms_database.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/util/options.cpp diff | blob | history
src/util/options.h diff | blob | history