Handle recursive singleton case for codatatypes, add regression. Simplify implementa...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 13 Feb 2015 13:12:32 +0000 (14:12 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 13 Feb 2015 13:12:41 +0000 (14:12 +0100)
commit82fbac8829cbc41927216b36ab064b50e50b2fa0
tree346361d002c109b8ac2254f4f215a12dfc7643d2
parent3ba153b4be4c2fe8ad7decf8ebc7cf5d8815a0e9
Handle recursive singleton case for codatatypes, add regression.  Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
12 files changed:
src/parser/parser.cpp
src/theory/datatypes/datatypes_rewriter.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/unconstrained_simplifier.cpp
src/util/cardinality.h
src/util/datatype.cpp
src/util/datatype.h
test/regress/regress0/datatypes/Makefile.am
test/regress/regress0/datatypes/stream-singleton.smt2 [new file with mode: 0644]
test/unit/parser/parser_black.h