projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 01cff04) | patch
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies;...
authorMorgan Deters <mdeters@cs.nyu.edu>
Fri, 7 Mar 2014 15:24:04 +0000 (10:24 -0500)
committerMorgan Deters <mdeters@cs.nyu.edu>
Sat, 8 Mar 2014 04:48:49 +0000 (23:48 -0500)
commitd01269e2d5a02952fbda74dcd9629acfbf23dfd4
treed8f2a90ddd94ade15edf84b48523e7ff76f78554tree
parent01cff049fac316d84ee05f747975a26b04e9c3a2commit | diff
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
18 files changed:
src/expr/node.cpp diff | blob | history
src/expr/node.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/ite_utilities.cpp diff | blob | history
src/theory/ite_utilities.h diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/util/ite_removal.cpp diff | blob | history
src/util/ite_removal.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/bug548a.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/fmf-bound-int.smt2 [new file with mode: 0644] blob
test/regress/regress0/rewriterules/Makefile.am diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history