diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 17:59:33 +0000 |
commit | 3d2b33d66998261f9369cccc098140f64bc8b417 (patch) | |
tree | 9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/expr/mkexpr | |
parent | 92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff) |
portfolio merge
Diffstat (limited to 'src/expr/mkexpr')
-rwxr-xr-x | src/expr/mkexpr | 4 |
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 |