projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6c58094) | patch
Enable bounded set membership with --fmf-bound. Map to term models for bounded set...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 15 Aug 2016 16:30:17 +0000 (11:30 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 15 Aug 2016 16:30:17 +0000 (11:30 -0500)
commitbaaab488c597e3e30dd3b929a5a612ba7fd660af
treeb7841c415997360b5d18218821ce3587b834ba84tree
parent6c58094be960ddca3a2187081bac769da61cc2afcommit | diff
Enable bounded set membership with --fmf-bound. Map to term models for bounded set membership.
src/options/quantifiers_options diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/quantifiers/bounded_integers.h diff | blob | history
src/theory/quantifiers/full_model_check.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_engine.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history
test/regress/regress0/quantifiers/bi-artm-s.smt2 diff | blob | history