summaryrefslogtreecommitdiff
path: root/src/expr/mkexpr
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-02-20 17:59:33 +0000
committerMorgan Deters <mdeters@gmail.com>2012-02-20 17:59:33 +0000
commit3d2b33d66998261f9369cccc098140f64bc8b417 (patch)
tree9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/expr/mkexpr
parent92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff)
portfolio merge
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