BV/Int propagations #824
Assignees
Milestone
Comments
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Nov 23, 2023
This is a follow-up to OCamlPro#954 Somehow convinced myself that the cases where we perform simplifications were fine because we would only be simplifying into a subterm, but that is obviously not the case due to negation. Let's just do the safe thing and always return the original term with the appropriate equalities. All of this code should be removed in favor of doing these computations in the relations instead anyways, which would make sure we always treat [bv2nat] in the same way for literals and after substitution (see also OCamlPro#824 )
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Nov 24, 2023
This is a follow-up to OCamlPro#954 Somehow convinced myself that the cases where we perform simplifications were fine because we would only be simplifying into a subterm, but that is obviously not the case due to negation. Let's just do the safe thing and always return the original term with the appropriate equalities. All of this code should be removed in favor of doing these computations in the relations instead anyways, which would make sure we always treat [bv2nat] in the same way for literals and after substitution (see also OCamlPro#824 )
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Nov 24, 2023
This is a follow-up to OCamlPro#954 Somehow convinced myself that the cases where we perform simplifications were fine because we would only be simplifying into a subterm, but that is obviously not the case due to negation. Let's just do the safe thing and always return the original term with the appropriate equalities. All of this code should be removed in favor of doing these computations in the relations instead anyways, which would make sure we always treat [bv2nat] in the same way for literals and after substitution (see also OCamlPro#824 )
bclement-ocp
added a commit
that referenced
this issue
Nov 24, 2023
This is a follow-up to #954 Somehow convinced myself that the cases where we perform simplifications were fine because we would only be simplifying into a subterm, but that is obviously not the case due to negation. Let's just do the safe thing and always return the original term with the appropriate equalities. All of this code should be removed in favor of doing these computations in the relations instead anyways, which would make sure we always treat [bv2nat] in the same way for literals and after substitution (see also #824 )
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When we have (dis|in)equalities between
int2bv/bv2natterms we should propagate the relevant information to the other theory. For instance, if we havebv2nat(x) = bv2nat(y), we should be able to learnx = y. This is the relational version of #801 (which is about computingint2bv/bv2natvalues when their argument is known).See also #749 for an incomplete implementation of this.
The text was updated successfully, but these errors were encountered: