mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

a pending issue from #4866

Browse source 
https://github.com/Z3Prover/z3/issues/4866#issuecomment-748658905
This commit is contained in:
Nikolaj Bjorner 2021-03-16 05:26:06 -07:00
parent dc5fa89de3
commit cb8c6ffafc
3 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/smt_internalizer.cpp
View file

@ -340,6 +340,8 @@ namespace smt {
void context::ensure_internalized(expr* e) { void context::ensure_internalized(expr* e) {
if (!e_internalized(e)) if (!e_internalized(e))
internalize(e, false); internalize(e, false);
if (is_app(e))
internalize_term(to_app(e));
} }
/** /**
@ -354,10 +356,9 @@ namespace smt {
void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) { void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) {
internalize_deep(exprs, num_exprs); internalize_deep(exprs, num_exprs);
for (unsigned i = 0; i < num_exprs; ++i) { for (unsigned i = 0; i < num_exprs; ++i)
internalize_rec(exprs[i], gate_ctx); internalize_rec(exprs[i], gate_ctx);
} }
}
void context::internalize_rec(expr * n, bool gate_ctx) { void context::internalize_rec(expr * n, bool gate_ctx) {
TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m) << "\n";); TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m) << "\n";);

4
src/smt/smt_theory.cpp
View file

@ -161,9 +161,9 @@ namespace smt {
} }
enode* theory::ensure_enode(expr* e) { enode* theory::ensure_enode(expr* e) {
if (!ctx.e_internalized(e)) { if (!ctx.e_internalized(e))
ctx.internalize(e, is_quantifier(e)); ctx.internalize(e, is_quantifier(e));
} ctx.ensure_internalized(e); // make sure theory variables are attached.
enode* n = ctx.get_enode(e); enode* n = ctx.get_enode(e);
ctx.mark_as_relevant(n); ctx.mark_as_relevant(n);
return n; return n;

3
src/smt/theory_seq.cpp
View file

@ -2810,6 +2810,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
f = m_sk.mk_prefix_inv(se1, se2); f = m_sk.mk_prefix_inv(se1, se2);
f = mk_concat(se1, f); f = mk_concat(se1, f);
propagate_eq(lit, f, se2, true); propagate_eq(lit, f, se2, true);
propagate_eq(lit, mk_len(f), mk_len(se2), false);
} }
else { else {
propagate_not_prefix(e); propagate_not_prefix(e);
@ -2823,6 +2824,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
f = m_sk.mk_suffix_inv(se1, se2); f = m_sk.mk_suffix_inv(se1, se2);
f = mk_concat(f, se1); f = mk_concat(f, se1);
propagate_eq(lit, f, se2, true); propagate_eq(lit, f, se2, true);
propagate_eq(lit, mk_len(f), mk_len(se2), false);
} }
else { else {
propagate_not_suffix(e); propagate_not_suffix(e);
@ -2842,6 +2844,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
expr_ref f2 = m_sk.mk_indexof_right(se1, se2); expr_ref f2 = m_sk.mk_indexof_right(se1, se2);
f = mk_concat(f1, se2, f2); f = mk_concat(f1, se2, f2);
propagate_eq(lit, f, e1, true); propagate_eq(lit, f, e1, true);
propagate_eq(lit, mk_len(f), mk_len(e1), false);
} }
else { else {
propagate_non_empty(lit, se2); propagate_non_empty(lit, se2);