mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 12:25:51 +00:00
Code Activity

fix #7634

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-27 23:57:57 -07:00
parent 24090fc48c
commit b502126ebc
2 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/rewriter/recfun_rewriter.cpp
View file

@ -37,15 +37,25 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
// check if there is an argument that is a constructor
// such that the recursive function can be partially evaluated.
// at most one kind of accessor is allowed to prevent recursive
// patterns that reconstruct the argument indirectly.
// This can be relaxed to omitting at least one accessor, and probably other patterns.
if (!safe_to_subst && !has_quantifiers(r)) {
datatype::util u(m);
auto is_decreasing = [&](unsigned i) {
bool is_dec = true;
unsigned idx = num_args - i - 1;
for (auto t : subterms::all(expr_ref(r, m)))
if (is_app(t) && any_of(*to_app(t), [&](expr* e) { return is_var(e) && to_var(e)->get_idx() == idx; }))
func_decl* dec_fun = nullptr;
for (auto t : subterms::all(expr_ref(r, m))) {
if (is_app(t) && any_of(*to_app(t), [&](expr* e) { return is_var(e) && to_var(e)->get_idx() == idx; })) {
if (!u.is_accessor(t) && !u.is_is(t) && !u.is_recognizer(t))
is_dec = false;
else if (u.is_accessor(t) && dec_fun && to_app(t)->get_decl() != dec_fun)
is_dec = false;
else if (u.is_accessor(t))
dec_fun = to_app(t)->get_decl();
}
}
return is_dec;
};
for (unsigned i = 0; i < num_args; ++i) {

2
src/sat/sat_solver.cpp
View file

@ -283,7 +283,7 @@ namespace sat {
m_stats.m_mk_var++;
bool_var v = m_justification.size();
if (!m_free_vars.empty()) {
if (!m_free_vars.empty() && false) {
v = m_free_vars.back();
m_free_vars.pop_back();
m_active_vars.push_back(v);