projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 65128ef) | patch
Expand definitions in theory datatypes, now has the expected semantics for incorrectl...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 10 Apr 2014 20:50:56 +0000 (15:50 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 10 Apr 2014 20:51:08 +0000 (15:51 -0500)
commit6ae07a91cdd4f20f8fdccd7e31d217c6ca34ee45
tree0f4f929831ba092b54a5919809a01f089e023b84tree
parent65128efc1d0a4c2007ebb7b47712888481c07843commit | diff
Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms.
17 files changed:
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/boolean_terms.cpp diff | blob | history
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/datatypes/kinds diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/datatypes/theory_datatypes_type_rules.h diff | blob | history
src/theory/quantifiers/options_handlers.h diff | blob | history
src/theory/quantifiers/quant_conflict_find.cpp diff | blob | history
src/theory/quantifiers/trigger.cpp diff | blob | history
src/theory/theory_model.cpp diff | blob | history
test/regress/regress0/datatypes/Makefile.am diff | blob | history
test/regress/regress0/datatypes/datatype1.cvc diff | blob | history
test/regress/regress0/datatypes/datatype3.cvc diff | blob | history
test/regress/regress0/datatypes/wrong-sel-simp.cvc diff | blob | history