From 5d3f48cc8d598508e1b56b265b31f702f4497311 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Jun 2021 09:51:31 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 847e56076..7c76b3f64 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1269,22 +1269,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const { case OP_RE_OPTION: i1 = get_info_rec(e->get_arg(0)); return i1.opt(); - case OP_RE_RANGE: { - lbool is_nullable = l_undef; - bool is_singleton = false; - bool is_interpreted = false; - zstring s1, s2; - expr* r1, *r2; - if (is_range(e, r1, r2) && - u.str.is_string(r1, s1) && u.str.is_string(r2, s2) && - s1.length() == 1 && s2.length() == 1 && s1[0] <= s2[0]) { - is_nullable = l_false; - is_singleton = true; - is_interpreted = true; - } - std::cout << is_nullable << "\n"; - return info(true, true, is_interpreted, true, true, true, is_singleton, is_nullable, 1, 0); - } + case OP_RE_RANGE: case OP_RE_FULL_CHAR_SET: case OP_RE_OF_PRED: //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat