From 4101652747f631d54915459c942d85e5e1f21bc3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Sep 2019 09:54:18 -0700 Subject: [PATCH] handle case where lower bound is above upper Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 6 +++++- src/ast/seq_decl_plugin.cpp | 3 --- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6af16dd06..d80732e82 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1824,6 +1824,10 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* expr* a = nullptr; switch (num_args) { case 1: + if (f->get_num_parameters() == 2 && f->get_parameter(0).get_int() > f->get_parameter(1).get_int()) { + result = m_util.re.mk_loop(args[0], f->get_parameter(1).get_int(), f->get_parameter(1).get_int()); + return BR_REWRITE1; + } // (loop (loop a lo hi) lo2 hi2) = (loop lo*lo2 hi*hi2) if (m_util.re.is_loop(args[0], a, lo, hi) && f->get_num_parameters() == 2) { result = m_util.re.mk_loop(a, f->get_parameter(0).get_int() * lo, f->get_parameter(1).get_int() * hi); @@ -1864,7 +1868,7 @@ br_status seq_rewriter::mk_re_loop(func_decl* f, unsigned num_args, expr* const* break; case 3: if (m_autil.is_numeral(args[1], n1) && n1.is_unsigned() && - m_autil.is_numeral(args[2], n2) && n2.is_unsigned() && n1 <= n2) { + m_autil.is_numeral(args[2], n2) && n2.is_unsigned()) { result = m_util.re.mk_loop(args[0], n1.get_unsigned(), n2.get_unsigned()); return BR_REWRITE1; } diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 5d2628c60..f1158dd53 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -747,9 +747,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, if (num_parameters == 0 || num_parameters > 2 || !parameters[0].is_int() || (num_parameters == 2 && !parameters[1].is_int())) { m.raise_exception("Expecting two numeral parameters to function re-loop"); } - if (num_parameters == 2 && parameters[0].get_int() > parameters[1].get_int()) { - m.raise_exception("Lower bound cannot be higher than upper bound in loop specfication"); - } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); case 2: if (m_re != domain[0] || !arith_util(m).is_int(domain[1])) {