diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-29 23:42:41 +0000 |
commit | 349131957e91150c24a9c69f5e1f04e34494b0c6 (patch) | |
tree | 8012c2475dde1f1177f693643fb1a07e89c29538 /src/expr/mkmetakind | |
parent | ac8b46fe3b5256e387da724b7c3abfb59d25531e (diff) |
Added the capability to construct expressions by passing the operator instead of the kind, i.e.
Expr op = ..."f"...
em.mkExpr(op, children);
Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.
Diffstat (limited to 'src/expr/mkmetakind')
-rwxr-xr-x | src/expr/mkmetakind | 25 |
1 files changed, 17 insertions, 8 deletions
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 84d18e218..e8f3724f1 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -46,6 +46,7 @@ metakind_constHashes= metakind_constPrinters= metakind_ubchildren= metakind_lbchildren= +metakind_operatorKinds= seen_theory=false seen_theory_builtin=false @@ -86,7 +87,7 @@ function variable { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind VARIABLE "$1" 0 + register_metakind VARIABLE "$1" UNDEFINED_KIND 0 } function operator { @@ -95,7 +96,7 @@ function operator { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind OPERATOR "$1" "$2" + register_metakind OPERATOR "$1" UNDEFINED_KIND "$2" } function nonatomic_operator { @@ -104,16 +105,16 @@ function nonatomic_operator { lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind NONATOMIC_OPERATOR "$1" "$2" + register_metakind NONATOMIC_OPERATOR "$1" UNDEFINED_KIND "$2" } function parameterized { - # parameterized K #children ["comment"] + # parameterized K1 K2 #children ["comment"] lineno=${BASH_LINENO[0]} check_theory_seen - register_metakind PARAMETERIZED "$1" "$2" + register_metakind PARAMETERIZED "$1" "$2" "$3" } function constant { @@ -141,7 +142,7 @@ function constant { metakind_includes="${metakind_includes} #include \"$4\"" fi - register_metakind CONSTANT "$1" 0 + register_metakind CONSTANT "$1" UNDEFINED_KIND 0 metakind_constantMaps="${metakind_constantMaps} }/* CVC4::kind::metakind namespace */ }/* CVC4::kind namespace */ @@ -206,7 +207,11 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { function register_metakind { mk=$1 k=$2 - nc=$3 + k1=$3 + nc=$4 + + metakind_operatorKinds="${metakind_operatorKinds} kind::$k1, /* $k */ +"; if [ $mk = NONATOMIC_OPERATOR ]; then metakind_canbeatomic="${metakind_canbeatomic} false, /* $k */ @@ -290,6 +295,9 @@ while [ $# -gt 0 ]; do metakind_canbeatomic="${metakind_canbeatomic} /* from $b */ " + metakind_operatorKinds="${metakind_operatorKinds} + /* from $b */ +" source "$kf" check_theory_seen shift @@ -308,7 +316,8 @@ for var in \ metakind_constHashes \ metakind_constPrinters \ metakind_ubchildren \ - metakind_lbchildren; do + metakind_lbchildren \ + metakind_operatorKinds; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" done error=`expr "$text" : '.*\${\([^}]*\)}.*'` |