diff options
Diffstat (limited to 'src/theory/mktheorytraits')
-rwxr-xr-x | src/theory/mktheorytraits | 14 |
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]} |