projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a033e9f) | 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)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 6 Nov 2013 18:31:42 +0000 (12:31 -0600)
commitecf2e4ec0f623a46f89b697d1afba81834455d95
tree5a25b61d77aa9e21b3347872b5aee9839594ec8btree
parenta033e9f6fb8d24a0d8db872904bbdc289ab1e98ccommit | 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