mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix #5032, reset substitution during fold transformation

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-15 14:14:25 -08:00
parent 6bd02e122b
commit c387863da1
3 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast.h
View file

@ -2453,6 +2453,12 @@ typedef obj_ref<app, ast_manager> app_ref;
typedef obj_ref<var,ast_manager> var_ref; typedef obj_ref<var,ast_manager> var_ref;
typedef app_ref proof_ref; typedef app_ref proof_ref;
inline expr_ref operator~(expr_ref const & e) {
if (e.m().is_not(e))
return expr_ref(to_app(e)->get_arg(0), e.m());
return expr_ref(e.m().mk_not(e), e.m());
}
// ----------------------------------- // -----------------------------------
// //
// ast_vector (smart pointer vector) // ast_vector (smart pointer vector)

4
src/ast/recfun_decl_plugin.cpp
View file

@ -496,6 +496,7 @@ namespace recfun {
if (max_score <= 4) if (max_score <= 4)
break; break;
ptr_vector<sort> domain; ptr_vector<sort> domain;
ptr_vector<expr> args; ptr_vector<expr> args;
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
@ -508,9 +509,10 @@ namespace recfun {
func_decl* f = pd.get_def()->get_decl(); func_decl* f = pd.get_def()->get_decl();
expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m()); expr_ref new_body(m().mk_app(f, n, args.c_ptr()), m());
set_definition(subst, pd, n, vars, max_expr); set_definition(subst, pd, n, vars, max_expr);
subst.reset();
subst.insert(max_expr, new_body); subst.insert(max_expr, new_body);
result = subst(result); result = subst(result);
TRACEFN("substituted\n" << mk_pp(max_expr, m()) << "\n->\n" << new_body << "\n" << result); TRACEFN("substituted\n" << mk_pp(max_expr, m()) << "\n->\n" << new_body << "\n-result->\n" << result);
} }
return result; return result;
} }

2
src/smt/theory_char.cpp
View file

@ -258,7 +258,7 @@ namespace smt {
for (unsigned v = get_num_vars(); v-- > 0; ) { for (unsigned v = get_num_vars(); v-- > 0; ) {
expr* e = get_expr(v); expr* e = get_expr(v);
if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) { if (seq.is_char(e) && m_var2value[v] == UINT_MAX && get_char_value(v, c)) {
CTRACE("seq", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";); CTRACE("seq_verbose", seq.is_char(e), tout << mk_pp(e, m) << " root: " << get_enode(v)->is_root() << " is_value: " << get_char_value(v, c) << "\n";);
enode* r = get_enode(v)->get_root(); enode* r = get_enode(v)->get_root();
m_value2var.reserve(c + 1, null_theory_var); m_value2var.reserve(c + 1, null_theory_var);
theory_var u = m_value2var[c]; theory_var u = m_value2var[c];