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

1 files changed, 12 insertions, 2 deletions

diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 9672fc871..2056c6306 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -197,10 +197,14 @@ function properties {
 }
 
 function sort {
-  # sort TYPE cardinality ["comment"]
+  # sort TYPE cardinality [well-founded ground-term header | not-well-founded] ["comment"]
   lineno=${BASH_LINENO[0]}
   check_theory_seen
-  register_sort "$1" "$2" "$3"
+  if [ "$3" = well-founded ]; then
+    register_sort "$1" "$2" "$6"
+  else
+    register_sort "$1" "$2" "$4"
+  fi
 }
 
 function cardinality {
@@ -209,6 +213,12 @@ function cardinality {
   check_theory_seen
 }
 
+function well-founded {
+  # well-founded TYPE wellfoundedness-computer [header]
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
+}
+
 function variable {
   # variable K ["comment"]
   lineno=${BASH_LINENO[0]}