projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4ab031f) | patch
Bug fixes for bounded integer quantification. Current best strategy is to turn off...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 6 Nov 2013 18:31:31 +0000 (12:31 -0600)
committerTianyi Liang <tianyi-liang@uiowa.edu>
Wed, 6 Nov 2013 23:19:09 +0000 (17:19 -0600)
commit6d2def1c2e44974227fb06d3aa199722a4193a04
tree1020f03dfbef0e9e5c8759b888dd75885aa2ac37tree
parent4ab031f6173ca18aa21c938bc2672ef25c283428commit | diff
Bug fixes for bounded integer quantification.  Current best strategy is to turn off MBQI.  Disable relevant triggers by default.
13 files changed:
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/full_model_check.h diff | blob | history
src/theory/quantifiers/instantiation_engine.cpp diff | blob | history
src/theory/quantifiers/model_builder.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/uf/theory_uf_model.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history