From 49ee570b09047cbea94f7d26e3df10c86c9ce596 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Jan 2023 19:16:46 -0800 Subject: [PATCH] split into separate function Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/array_rewriter.cpp | 17 ++++++++++++----- src/ast/rewriter/array_rewriter.h | 9 +++++---- 2 files changed, 17 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp index 85cdeb50a..58e807fd7 100644 --- a/src/ast/rewriter/array_rewriter.cpp +++ b/src/ast/rewriter/array_rewriter.cpp @@ -196,10 +196,9 @@ bool array_rewriter::squash_store(unsigned n, expr* const* args, expr_ref& resul } -br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, expr_ref & result) { - SASSERT(num_args >= 2); - expr *arg0 = args[0]; +br_status array_rewriter::mk_select_same_store(unsigned num_args, expr * const * args, expr_ref & result) { expr_ref tmp(m()); + expr *arg0 = args[0]; bool first = true; #define RET(x, status) \ @@ -228,9 +227,9 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, if (first) { result = to_app(arg0)->get_arg(num_args); first = false; - } else if (result != to_app(arg0)->get_arg(num_args)) { - goto exit; } + else if (result != to_app(arg0)->get_arg(num_args)) + goto exit; arg0 = to_app(arg0)->get_arg(0); continue; } @@ -281,6 +280,14 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, } exit: + return BR_FAILED; +} + +br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, expr_ref & result) { + SASSERT(num_args >= 2); + br_status st = mk_select_same_store(num_args, args, result); + if (st != BR_FAILED) + return st; result.reset(); if (m_util.is_store(args[0])) { diff --git a/src/ast/rewriter/array_rewriter.h b/src/ast/rewriter/array_rewriter.h index 4e52b237e..689aea1f9 100644 --- a/src/ast/rewriter/array_rewriter.h +++ b/src/ast/rewriter/array_rewriter.h @@ -46,6 +46,11 @@ class array_rewriter { expr_ref expand_store(expr* s); bool squash_store(unsigned n, expr* const* args, expr_ref& result); + + br_status mk_store_core(unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_select_core(unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_select_same_store(unsigned num_args, expr * const * args, expr_ref & result); + br_status mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); public: array_rewriter(ast_manager & m, params_ref const & p = params_ref()): @@ -63,10 +68,6 @@ public: br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - br_status mk_store_core(unsigned num_args, expr * const * args, expr_ref & result); - br_status mk_select_core(unsigned num_args, expr * const * args, expr_ref & result); - br_status mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - void mk_store(unsigned num_args, expr * const * args, expr_ref & result); void mk_select(unsigned num_args, expr * const * args, expr_ref & result); void mk_map(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);