split into separate function

Signed-off-by: Nikolaj Bjorner <[email protected]>
hgvk94 · Mar 27, 2023 · c3e9f27 · c3e9f27
1 parent e7d906f
commit c3e9f27
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 9 deletions.
diff --git 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
@@ -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 @@ class array_rewriter {
 
     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);