projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4a919f0) | patch
Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant bounds...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 4 Jun 2013 17:12:30 +0000 (12:12 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 4 Jun 2013 17:12:41 +0000 (12:12 -0500)
commit25a01d31bffcdcc339dce332ac893460b5f4cdcf
tree2ea257c8240aaec6155992c5dc0231c2f6ef854dtree
parent4a919f014c3b6bcdca6bd2f91cfc14d50445887ccommit | diff
Add partial support for MBQI with arrays when using --fmf-fmc.  Fix constant bounds for bounded integers.
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/first_order_model.h 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/rep_set.h diff | blob | history