Fixed UP expression registration #7656
Conversation
src/smt/theory_user_propagator.cpp
Outdated
| enode* n = ensure_enode ? this->ensure_enode(e) : ctx.get_enode(e); | ||
| ctx.get_rewriter()(term, r); | ||
| TRACE("user_propagate", tout << "add " << mk_bounded_pp(term, m) << "\n"); | ||
| enode* n = ensure_enode ? this->ensure_enode(r) : ctx.get_enode(r); |
There was a problem hiding this comment.
what if r is a quantified formula?
It is only possible to create E-nodes with quantifier-free formulas.
The deleted code will take care of this.
Seems you want the deleted code when there are quantifiers.
And for that matter the old code seems also incorrect.
There was a problem hiding this comment.
There is a general problem with registering new terms (in addition to the fact that the raw pointer is stored; I just copied some part from my fork):
Asserting "aux-expr = r" for some fresh constant "aux-expr" introduces a problem: if someone registers the same ast multiple times, they get a new constant every time.
So registering, e.g., ast/expr "A & B" several times (as it might have been forgotten upon backtracking), and using that expression as a justification is not possible, as Z3 will internally refer to a different Boolean variable for "A & B" every time. Also, Z3 might eventually forget the "aux-expr = r" lemma on backtracking, such that the relation between "aux-expr" and "r" is forgotten. Registering it again does not work, as Z3 would just introduce a fresh aux-expr in that case.
My (for sure not optimal) solution I used so far in my fork is to return the rewritten ast, rather than introducing an auxiliary term (admittedly, I did not think of quantifiers, in which case this solution does not work) and received callbacks/gave justifications in term of the returned ast, rather than the passed one.
Do you have an idea how to solve this?
There was a problem hiding this comment.
Got it, this part is fixable by caching, and for ground expressions by using e_internalized.
|
with the updates, the new code is equivalent to the old code |
No description provided.