From 081c62d006306ea7db52b3949dc0e21f55fc458b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Mar 2022 17:08:49 -0800 Subject: [PATCH] allow range comparison for bit-vectors and int/real --- src/ast/char_decl_plugin.cpp | 9 +++++++++ src/ast/rewriter/seq_rewriter.cpp | 4 ++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 2ab4def9aa8..029312ba326 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -16,6 +16,7 @@ Module Name: --*/ #include "util/gparams.h" +#include "ast/bv_decl_plugin.h" #include "ast/char_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/ast_pp.h" @@ -164,6 +165,14 @@ app* char_decl_plugin::mk_le(expr* a, expr* b) { unsigned v1 = 0, v2 = 0; if (a == b) return m_manager->mk_true(); + bv_util bv(*m_manager); + if (bv.is_bv(a)) + return bv.mk_ule(a, b); + arith_util arith(*m_manager); + if (arith.is_int_real(a)) + return arith.mk_le(a, b); + if (a->get_sort() != char_sort()) + throw default_exception("range comparison is only supported for bit-vectors, int, real and characters"); bool c1 = is_const_char(a, v1); bool c2 = is_const_char(b, v2); if (c1 && c2) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index b5f0e14754b..02faebba5d0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3128,8 +3128,8 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref expr_ref range(m()); expr_ref psi(m().mk_false(), m()); if (str().is_unit_string(r1, c1) && str().is_unit_string(r2, c2)) { - SASSERT(u().is_char(c1)); - SASSERT(u().is_char(c2)); + // SASSERT(u().is_char(c1)); + // SASSERT(u().is_char(c2)); // case: c1 <= e <= c2 range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2))); psi = simplify_path(e, m().mk_and(path, range));