From a65efb682ba96a313488b9ad5aa5c279ed7c1249 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 10:38:13 -0800 Subject: [PATCH] avoid const in ml Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/ast/recfun_decl_plugin.cpp | 5 ++++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 42bfcc37e..73edccad1 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -90,7 +90,7 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I # Mapping to ML types Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', - BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'char const*' } + BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'char*' } next_type_id = FIRST_OBJ_ID diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index b920eaa89..b11b945fd 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -375,7 +375,10 @@ namespace recfun { SASSERT(n_vars == d->get_arity()); is_imm_pred is_i(*u); - d->compute_cases(*u, r, is_i, n_vars, vars, rhs); +#if 0 + expr_ref reduced_rhs = preprocess_ites(*u, r, n_vars, vars, rhs); + d->compute_cases(*u, r, is_i, n_vars, vars, reduced_rhs); +#endif } namespace decl {