Monday tasks:
authorMorgan Deters <mdeters@gmail.com>
Mon, 25 Apr 2011 23:44:00 +0000 (23:44 +0000)
committerMorgan Deters <mdeters@gmail.com>
Mon, 25 Apr 2011 23:44:00 +0000 (23:44 +0000)
commit97111ecb8681838f2d201420cda12ca9fc7184ed
treeeee78a3ff75c1c9535b1db89ed273116a6ef3542
parentde164c9308f6461472b95c23aae68d9d9686d8ae
Monday tasks:

* new "well-foundedness" type property (like cardinality) specified in
  Theory kinds files; specifies well-foundedness and a ground term

* well-foundedness / finite checks in Datatypes now superseded by type
  system isFinite(), isWellFounded(), mkGroundTerm().

* new "RecursionBreaker" template class, a convenient class that keeps
  a "seen" trail without you having to pass it around (which is
  difficult in cases of mutual recursion) of the idea of passing
  around a "seen" trail
30 files changed:
src/expr/expr_manager_scope.h
src/expr/expr_manager_template.cpp
src/expr/mkexpr
src/expr/mkkind
src/expr/mkmetakind
src/expr/type.cpp
src/expr/type.h
src/expr/type_node.cpp
src/expr/type_node.h
src/expr/type_properties_template.h
src/smt/smt_engine.cpp
src/theory/arith/kinds
src/theory/arrays/kinds
src/theory/booleans/kinds
src/theory/builtin/kinds
src/theory/builtin/theory_builtin_type_rules.h
src/theory/datatypes/kinds
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/datatypes/theory_datatypes_type_rules.h
src/theory/mkrewriter
src/theory/mktheorytraits
src/theory/uf/kinds
src/util/Makefile.am
src/util/datatype.cpp
src/util/datatype.h
src/util/recursion_breaker.h [new file with mode: 0644]
test/unit/Makefile.am
test/unit/util/datatype_black.h
test/unit/util/recursion_breaker_black.h [new file with mode: 0644]