From 97af74d8cbc79a727d5eb94d0b48b011566132f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Apr 2020 14:19:26 -0700 Subject: [PATCH] fix #3917 remove non-native mode for recfun Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 6 ------ src/muz/base/rule_properties.cpp | 3 ++- src/smt/params/smt_params_helper.pyg | 1 - 3 files changed, 2 insertions(+), 8 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 2a4c29688..2aba7c89f 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -928,12 +928,6 @@ void cmd_context::insert_rec_fun_as_axiom(func_decl *f, expr_ref_vector const& b void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, svector const& ids, expr* rhs) { - if (gparams::get_value("smt.recfun.native") != "true") { - // just use an axiom - insert_rec_fun_as_axiom(f, binding, ids, rhs); - return; - } - TRACE("recfun", tout<< "define recfun " << f->get_name() << " = " << mk_pp(rhs, m()) << "\n";); recfun::decl::plugin& p = get_recfun_plugin(); diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 7923eeae4..f0998747a 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -73,10 +73,11 @@ void rule_properties::check_quantifier_free() { } static const std::string qkind_str(quantifier_kind qkind) { - switch(qkind) { + switch (qkind) { case forall_k: return "FORALL"; case exists_k: return "EXISTS"; case lambda_k: return "LAMBDA"; + default: UNREACHABLE(); return ""; } } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 9cf0d0bb0..a2300238f 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -120,6 +120,5 @@ def_module_params(module_name='smt', ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'), ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'), ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'), - ('recfun.native', BOOL, True, 'use native rec-fun solver'), ('recfun.depth', UINT, 2, 'initial depth for maxrec expansion') ))