projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3c4c442) | patch
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and...
authorajreynol <andrew.j.reynolds@gmail.com>
Mon, 8 Feb 2016 21:49:14 +0000 (15:49 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Mon, 8 Feb 2016 21:50:20 +0000 (15:50 -0600)
commit2dd6292b73e4e19be2e261c7fe5664bd2b0149bd
tree0f4956ec068972da8c8d1c708df7c8b2f7a07f3atree
parent3c4c4420ebae4d27d53084453591363942eb4d2ecommit | diff
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.
19 files changed:
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.cpp diff | blob | history
src/theory/datatypes/type_enumerator.h diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.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/quantifiers/term_database.cpp diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model.h diff | blob | history
src/theory/uf/theory_uf.cpp diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/nun-0208-to.smt2 [new file with mode: 0644] blob
test/regress/regress0/quantifiers/Makefile.am diff | blob | history
test/regress/regress0/quantifiers/cdt-0208-to.smt2 [new file with mode: 0644] blob