projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 08294c3) | patch
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves...
authorMorgan Deters <mdeters@cs.nyu.edu>
Mon, 17 Feb 2014 23:59:39 +0000 (18:59 -0500)
committerMorgan Deters <mdeters@cs.nyu.edu>
Tue, 4 Mar 2014 12:56:20 +0000 (07:56 -0500)
commited87e0c1ccb0cb93cdedf5229c6a2b47af77743c
treeb7c0efe878b82e6aff545b1d2fd52a02120f5813tree
parent08294c3914e4e87f3c5c1eda60e6ea259b789f55commit | diff
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).
17 files changed:
src/prop/prop_engine.cpp diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/output_channel.h diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/symmetry_breaking.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.cpp diff | blob | history
src/theory/quantifiers/theory_quantifiers.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/rewriterules/theory_rewriterules.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/theory/theory_test_utils.h diff | blob | history
src/util/statistics_registry.h diff | blob | history
test/unit/theory/theory_engine_white.h diff | blob | history
test/unit/theory/theory_white.h diff | blob | history