summaryrefslogtreecommitdiff
path: root/src/expr/mkexpr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-xsrc/expr/mkexpr4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 69f7019ab..0cae68ed0 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -60,6 +60,7 @@ getConst_instantiations=
getConst_implementations=
mkConst_instantiations=
mkConst_implementations=
+exportConstant_cases=
seen_theory=false
seen_theory_builtin=false
@@ -193,6 +194,8 @@ template <> $2 const & Expr::getConst() const {
return d_node->getConst< $2 >();
}
"
+ exportConstant_cases="${exportConstant_cases}
+ case $1: return to->mkConst(n.getConst< $2 >());"
}
function check_theory_seen {
@@ -244,6 +247,7 @@ for var in \
getConst_implementations \
mkConst_instantiations \
mkConst_implementations \
+ exportConstant_cases \
typechecker_includes \
typerules \
; do
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback