summaryrefslogtreecommitdiff
path: root/src/expr/mkkind
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2011-04-20 05:37:38 +0000
committerMorgan Deters <mdeters@gmail.com>2011-04-20 05:37:38 +0000
commit12c1e41862e4b12c3953272416a1edc103d299ee (patch)
tree9c7d3a044c33ffc3be177e6ca692eb4149add27c /src/expr/mkkind
parent08df44e6b61999a14dd24a7a134146694dcb3596 (diff)
Tuesday end-of-day commit.
Expected performance impact outside of datatypes/CVC parser is negligible. * CVC language LAMBDA, functional LET, type LET, precedence fixes, bitvectors, and arrays, with partial parsing support also for quantifiers, tuples, subranges, subtypes, and records * support for complex recursive DATATYPE selectors, e.g. tree = node(children:ARRAY INT OF tree) | leaf(data:INT) these are complicated because they have to be left unresolved at parse time and dealt with in a second pass. * bugfix for Exprs/Types that occurred when setting them to null (not Nodes/TypeNodes, just Exprs/Types). * Cleanup/code review items
Diffstat (limited to 'src/expr/mkkind')
-rwxr-xr-xsrc/expr/mkkind14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/expr/mkkind b/src/expr/mkkind
index f7f6ba836..fa80894b2 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -73,9 +73,9 @@ function theory {
fi
theory_id="$1"
- theory_enum="$1,
- ${theory_enum}"
- theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break;
+ theory_enum="${theory_enum} $1,
+"
+ theory_descriptions="${theory_descriptions} case ${theory_id}: out << \"${theory_id}\"; break;
"
}
@@ -144,11 +144,11 @@ function register_sort {
id=$1
comment=$2
- type_constant_list="${type_constant_list} ${id}, /**< ${comment} */
+ type_constant_list="${type_constant_list} ${id}, /**< ${comment} */
"
- type_constant_descriptions="${type_constant_descriptions} case $id: out << \"${comment}\"; break;
+ 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;
+ type_constant_to_theory_id="${type_constant_to_theory_id} case $id: return $theory_id; break;
"
}
@@ -161,7 +161,7 @@ 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;
+ kind_to_theory_id="${kind_to_theory_id} case kind::$r: return $theory_id; break;
"
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback