diff options
Diffstat (limited to 'src/theory/mktheorytraits')
-rwxr-xr-x | src/theory/mktheorytraits | 47 |
1 files changed, 46 insertions, 1 deletions
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 297df1f36..3607d5232 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -16,9 +16,11 @@ copyright=2010-2012 +filename=`basename "$1" | sed 's,_template,,'` + cat <<EOF /********************* */ -/** theory_traits.h +/** $filename ** ** Copyright $copyright The AcSys Group, New York University, and as below. ** @@ -40,6 +42,9 @@ theory_includes= theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\ " +type_enumerator_includes= +mk_type_enumerator_cases= + theory_has_check="false" theory_has_propagate="false" theory_has_staticLearning="false" @@ -61,6 +66,9 @@ instantiator_header= theory_id= theory_class= +type_constants= +type_kinds= + seen_theory=false seen_theory_builtin=false @@ -177,7 +185,39 @@ struct TheoryTraits<${theory_id}> { theory_id= theory_class= + type_constants= + type_kinds= + + lineno=${BASH_LINENO[0]} +} + +function enumerator { + # enumerator KIND enumerator-class header lineno=${BASH_LINENO[0]} + check_theory_seen + type_enumerator_includes="${type_enumerator_includes} +#line $lineno \"$kf\" +#include \"$3\"" + if expr "$type_constants" : '.* '"$1"' ' &>/dev/null; then + mk_type_enumerator_type_constant_cases="${mk_type_enumerator_type_constant_cases} +#line $lineno \"$kf\" + case $1: +#line $lineno \"$kf\" + return new $2(type); +" + elif expr "$type_kinds" : '.* '"$1"' ' &>/dev/null; then + mk_type_enumerator_cases="${mk_type_enumerator_cases} +#line $lineno \"$kf\" + case kind::$1: +#line $lineno \"$kf\" + return new $2(type); +" + else + echo "$kf:$lineno: error: don't know anything about $1; enumerator must appear after definition" >&2 + echo "type_constants: $type_constants" >&2 + echo "type_kinds : $type_kinds" >&2 + exit 1 + fi } function typechecker { @@ -285,6 +325,7 @@ function register_sort { comment=$3 type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; " + type_constants="${type_constants} $1 " } function register_kind { @@ -293,6 +334,7 @@ function register_kind { comment=$3 kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; " + type_kinds="${type_kinds} $1 " } function check_theory_seen { @@ -342,6 +384,9 @@ for var in \ theory_for_each_macro \ theory_includes \ template \ + type_enumerator_includes \ + mk_type_enumerator_type_constant_cases \ + mk_type_enumerator_cases \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done |