diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /src/expr/mkkind | |
parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'src/expr/mkkind')
-rwxr-xr-x | src/expr/mkkind | 64 |
1 files changed, 58 insertions, 6 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind index ab80224eb..d790a0195 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -37,10 +37,18 @@ template=$1; shift kind_decls= kind_printers= +kind_to_theory_id= + +type_constant_descriptions= +type_constant_list= +type_constant_to_theory_id= seen_theory=false seen_theory_builtin=false +theory_enum= +theory_descriptions= + function theory { # theory T header @@ -49,20 +57,50 @@ function theory { # this script doesn't care about the theory class information, but # makes does make sure it's there seen_theory=true - if [ "$1" = builtin ]; then + if [ "$1" = THEORY_BUILTIN ]; then if $seen_theory_builtin; then echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2 exit 1 fi seen_theory_builtin=true - elif [ -z "$1" -o -z "$2" ]; then + elif [ -z "$1" -o -z "$2" -o -z "$3" ]; then echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2 exit 1 - elif ! expr "$1" : '\(::*\)' >/dev/null; then - echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 - elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then + elif ! expr "$2" : '\(::*\)' >/dev/null; then + echo "$kf:$lineno: warning: theory class \`$2' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2 + elif ! expr "$2" : '\(::CVC4::theory::*\)' >/dev/null; then echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2 fi + + theory_id="$1" + theory_enum="$1, + ${theory_enum}" + theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break; +" +} + +function properties { + # rewriter class header + lineno=${BASH_LINENO[0]} +} + +function endtheory { + # endtheory + lineno=${BASH_LINENO[0]} +} + +function rewriter { + # properties prop* + lineno=${BASH_LINENO[0]} +} + +function sort { + # sort TYPE ["comment"] + + lineno=${BASH_LINENO[0]} + + check_theory_seen + register_sort "$1" "$2" } function variable { @@ -101,6 +139,18 @@ function constant { register_kind "$1" 0 "$5" } +function register_sort { + id=$1 + comment=$2 + + type_constant_list="${type_constant_list} ${id}, /**< ${comment} */ +" + type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break; +" + type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break; +" +} + function register_kind { r=$1 nc=$2 @@ -110,6 +160,8 @@ function register_kind { " kind_printers="${kind_printers} case $r: out << \"$r\"; break; " + kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break; +" } function check_theory_seen { @@ -144,7 +196,7 @@ check_builtin_theory_seen ## output text=$(cat "$template") -for var in kind_decls kind_printers; do +for var in kind_decls kind_printers kind_to_theory_id theory_enum type_constant_list type_constant_descriptions type_constant_to_theory_id theory_descriptions; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` |