mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

split into separate function

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-08 19:16:46 -08:00
parent 5899fe3cea
commit 49ee570b09
2 changed files with 17 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/ast/rewriter/array_rewriter.cpp
View file

@ -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])) {

9
src/ast/rewriter/array_rewriter.h
View file

@ -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);