projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7391759) | patch
Multiple fixes for datatypes theory solver: add support for parametric datatypes...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 7 Oct 2013 15:02:57 +0000 (10:02 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 7 Oct 2013 15:02:57 +0000 (10:02 -0500)
commit2f716d8e5eaf4a75c2cf2e431b96ac1f3c9b8a5f
treed3c3433a21be90a0ef5d03d1844f212f6a22c08atree
parent73917595b8f0a2fadfb9616f38a26e32afc25a32commit | diff
Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly.  Add representive flattening for quantifiers (currently disabled). Other minor cleanup.
src/smt/smt_engine.cpp diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/datatypes/type_enumerator.h 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/quantifiers_engine.h diff | blob | history