summaryrefslogtreecommitdiff
path: root/src/theory/mktheorytraits
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/mktheorytraits')
-rwxr-xr-xsrc/theory/mktheorytraits14
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]}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback