diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-30 23:55:18 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-30 23:55:18 +0000 |
commit | cb9a9b98b018106a02b31f2442f347a944d8dda8 (patch) | |
tree | 1669047e13e1224114e9fcea83b212dd6d72836d /src/expr/mkmetakind | |
parent | 349131957e91150c24a9c69f5e1f04e34494b0c6 (diff) |
Fix for bug 115, mapping was going in the wrong direction.
Diffstat (limited to 'src/expr/mkmetakind')
-rwxr-xr-x | src/expr/mkmetakind | 23 |
1 files changed, 14 insertions, 9 deletions
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index e8f3724f1..4915a17ec 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -87,7 +87,7 @@ function variable { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind VARIABLE "$1" UNDEFINED_KIND 0 + register_metakind VARIABLE "$1" 0 } function operator { @@ -96,7 +96,7 @@ function operator { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind OPERATOR "$1" UNDEFINED_KIND "$2" + register_metakind OPERATOR "$1" "$2" } function nonatomic_operator { @@ -105,7 +105,7 @@ function nonatomic_operator { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind NONATOMIC_OPERATOR "$1" UNDEFINED_KIND "$2" + register_metakind NONATOMIC_OPERATOR "$1" "$2" } function parameterized { @@ -114,7 +114,8 @@ function parameterized { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind PARAMETERIZED "$1" "$2" "$3" + register_metakind PARAMETERIZED "$1" "$3" + registerOperatorToKind "$1" "$2" } function constant { @@ -142,7 +143,7 @@ function constant { metakind_includes="${metakind_includes} #include \"$4\"" fi - register_metakind CONSTANT "$1" UNDEFINED_KIND 0 + register_metakind CONSTANT "$1" 0 metakind_constantMaps="${metakind_constantMaps} }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ @@ -204,14 +205,18 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { " } +function registerOperatorToKind { + operatorKind=$1 + applyKind=$2 + metakind_operatorKinds="${metakind_operatorKinds} case kind::$applyKind: return kind::$operatorKind; +"; +} + function register_metakind { mk=$1 k=$2 - k1=$3 - nc=$4 + nc=$3 - metakind_operatorKinds="${metakind_operatorKinds} kind::$k1, /* $k */ -"; if [ $mk = NONATOMIC_OPERATOR ]; then metakind_canbeatomic="${metakind_canbeatomic} false, /* $k */ |