projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fd38441) | patch
Change internal representative selection for finite domains that do not involve unint...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 16 Mar 2016 18:57:53 +0000 (13:57 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 16 Mar 2016 18:57:53 +0000 (13:57 -0500)
commiteb27070783709a410e6655ba9af6da6de5b0da9d
treec4fcb9203e2e72c9a96a51641ac15207f292a75btree
parentfd3844131f334e929bfb04eb2dcb6229cf1190cdcommit | diff
Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.
src/theory/quantifiers/full_model_check.cpp diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers/term_database.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history