From 72c89e1a4e188c7bd07747853b526539ff307105 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Sep 2025 15:58:48 -0700 Subject: [PATCH] fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.cpp | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 9e154f9dc..f90768c0a 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -776,10 +776,26 @@ namespace datalog { array_util ar; DL_ENGINE m_engine_type; - bool is_large_bv(sort* s) { + bool is_large_bv(expr *e) { + sort *s = e->get_sort(); + if (bv.is_bv_sort(s)) { + unsigned sz = bv.get_bv_size(s); + if (sz > 24) + return true; + } + if (is_app(e)) { + unsigned sz = 0; + for (auto arg : *to_app(e)) { + if (bv.is_bv(arg)) + sz += bv.get_bv_size(arg->get_sort()); + } + if (sz > 24) + return true; + } return false; } + public: engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), ar(m), m_engine_type(DATALOG_ENGINE) {} @@ -795,7 +811,7 @@ namespace datalog { else if (dt.is_datatype(e->get_sort())) { m_engine_type = SPACER_ENGINE; } - else if (is_large_bv(e->get_sort())) { + else if (is_large_bv(e)) { m_engine_type = SPACER_ENGINE; } else if (!e->get_sort()->get_num_elements().is_finite()) {