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

build

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-12-04 10:38:24 -08:00
parent b76ed6a47f
commit ead2a46a88
4 changed files with 46 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/poly_rewriter_def.h
View file

@ -292,7 +292,7 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
new_add_args.push_back(mk_mul_app(c, to_app(var)->get_arg(i)));
}
result = mk_add_app(new_add_args.size(), new_add_args.data());
TRACE("mul_bug", tout << "result: " << mk_bounded_pp(result, m,5) << "\n";);
TRACE("mul_bug", tout << "result: " << mk_bounded_pp(result, M(), 5) << "\n";);
return BR_REWRITE2;
}
}

7
src/ast/simplifiers/demodulator_simplifier.cpp
View file

@ -115,11 +115,12 @@ bool demodulator_simplifier::rewrite1(func_decl* f, expr_ref_vector const& args,
SASSERT(lhs->get_decl() == f);
TRACE("demodulator", tout << "Matching with demodulator: " << mk_pp(lhs, m) << std::endl; );
TRACE("demodulator", tout << "Matching with demodulator: " << mk_pp(lhs, m) << "\n");
if (m_match_subst(lhs, rhs, args.data(), np)) {
TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(rhs, m) << "\n===>\n" << np << "\n";);
m_dependencies.insert(i);
TRACE("demodulator_bug", tout << "succeeded...\n" << mk_pp(rhs, m) << "\n===>\n" << np << "\n");
if (dep(i))
m_dependencies.insert(i);
return true;
}
}

3
src/ast/simplifiers/demodulator_simplifier.h
View file

@ -54,7 +54,6 @@ class demodulator_simplifier : public dependent_expr_simplifier {
public:
demodulator_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st);
void reduce() override;
void reduce() override;
};

87
src/ast/substitution/demodulator_rewriter.cpp
View file

@ -669,53 +669,6 @@ void demodulator_rewriter::reschedule_processed(func_decl * f) {
}
}
bool demodulator_match_subst::can_rewrite(expr * n, expr * lhs) {
// this is a quick check, we just traverse d and check if there is an expression in d that is an instance of lhs of n'.
// we cannot use the trick used for m_processed, since the main loop would not terminate.
ptr_vector<expr> stack;
expr * curr;
expr_mark visited;
stack.push_back(n);
while (!stack.empty()) {
curr = stack.back();
if (visited.is_marked(curr)) {
stack.pop_back();
continue;
}
switch(curr->get_kind()) {
case AST_VAR:
visited.mark(curr, true);
stack.pop_back();
break;
case AST_APP:
if (for_each_expr_args(stack, visited, to_app(curr)->get_num_args(), to_app(curr)->get_args())) {
if ((*this)(lhs, curr))
return true;
visited.mark(curr, true);
stack.pop_back();
}
break;
case AST_QUANTIFIER:
if (visited.is_marked(to_quantifier(curr)->get_expr()))
stack.pop_back();
else
stack.push_back(to_quantifier(curr)->get_expr());
break;
default:
UNREACHABLE();
}
}
return false;
}
void demodulator_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
// use m_back_idx to find all demodulators d in m_fwd_idx that contains f {
@ -831,6 +784,46 @@ demodulator_match_subst::demodulator_match_subst(ast_manager & m):
m_subst(m) {
}
bool demodulator_match_subst::can_rewrite(expr* n, expr* lhs) {
// this is a quick check, we just traverse d and check if there is an expression in d that is an instance of lhs of n'.
// we cannot use the trick used for m_processed, since the main loop would not terminate.
ptr_vector<expr> stack;
expr* curr;
expr_mark visited;
stack.push_back(n);
while (!stack.empty()) {
curr = stack.back();
if (visited.is_marked(curr)) {
stack.pop_back();
continue;
}
switch (curr->get_kind()) {
case AST_VAR:
visited.mark(curr, true);
stack.pop_back();
break;
case AST_APP:
if (for_each_expr_args(stack, visited, to_app(curr)->get_num_args(), to_app(curr)->get_args())) {
if ((*this)(lhs, curr))
return true;
visited.mark(curr, true);
stack.pop_back();
}
break;
case AST_QUANTIFIER:
if (visited.is_marked(to_quantifier(curr)->get_expr()))
stack.pop_back();
else
stack.push_back(to_quantifier(curr)->get_expr());
break;
default:
UNREACHABLE();
}
}
return false;
}
/**
\brief Auxiliary functor used to implement optimization in match_args. See comment there.
*/