From a65efb682ba96a313488b9ad5aa5c279ed7c1249 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 10:38:13 -0800 Subject: [PATCH 1/3] 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 { From 88eb527b96895c7e08d37bb519e5768f0f7ae741 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 10:38:57 -0800 Subject: [PATCH 2/3] avoid const in ml Signed-off-by: Nikolaj Bjorner --- src/ast/recfun_decl_plugin.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index b11b945fd..b920eaa89 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -375,10 +375,7 @@ namespace recfun { SASSERT(n_vars == d->get_arity()); is_imm_pred is_i(*u); -#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 + d->compute_cases(*u, r, is_i, n_vars, vars, rhs); } namespace decl { From 80c98dfb1f692452c3798b0c68d19694e5c2c66b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2020 10:40:00 -0800 Subject: [PATCH 3/3] avoid const in ml Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 73edccad1..9e36507d7 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*' } + BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string' } next_type_id = FIRST_OBJ_ID