Improving reasoning for the BV theory #903
Assignees
Milestone
Comments
Halbaroth
added
reasoning
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Jan 26, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to flush the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Jan 26, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Feb 8, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Feb 9, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Feb 12, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Mar 4, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Mar 4, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Mar 12, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see OCamlPro#903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of OCamlPro#903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
|
Some updates here:
|
bclement-ocp
added a commit
that referenced
this issue
Mar 14, 2024
This patch rewrites the `Constraints_make` module in order to make it more flexible (this is preparatory step for dealing with arithmetic bit-vector constraints, see #903). More precisely: - Constraints no longer need to keep track of their own explanations, this is now entirely done by the `Constraints_make` functor. This makes it simpler to write `Constraint` modules, and avoid repeating boilerplate code to deal with explanation storage. Instead, the explanations are provided to the `Constraint` module in its `propagate` function. - The `Constraints_make` functor no longer need to know about constraint propagation. Instead, it simply keeps track of constraints that need to be propagated (pending constraints), and provides an API to iterate (and remove) the set of constraints to be propagated, letting the user take care of propagation proper. - The `Constraints_make` functor now tracks separately the constraint arguments and the leaves of said arguments. The leaves are used to know which constraints need to be updated during a substitution, and the arguments are used to mark as pending all constraints that apply to a given representative when its domain is updated (note that, for the bit-list domains, we actually store the domains at the leaves, so the arguments mapping is not used -- but this still makes the module more flexible in general, and in particular will allow to introduce arithmetic domains that need to be stored for all values, not only leaves, for the purpose of #903 in a future PR) The new design should make it easier to write `Constraint` modules. It also fixes a bug in the contract between the `Constraint` and `Domain` modules regarding substitution: the `Domain` modules was written under the assumption that constraints applying to `changed` domains would always be marked as pending upon substitution, but that is not true because we use functional representations where such updates are delayed, and hence the `changed` flag needs to be propagated after substitution (if appropriate).
|
I think we can remove the milestone on this issue because we do not plan extra works on it before the next release. |
|
Yes, we won't have constraint simplification for 2.6. Let's keep it to track |
|
I wanted to implement support for We already have many bv improvements, and these changes only add a small additional improvement for the bv2nat problems from our partners (~ 0.2% more problems solved) so it will have to wait for the next release. I'll try to cut a point release once it is integrated. |
|
I said this but then realised we are not even able to prove that |
|
Turns out this is somewhat rendered useless by #1228 which at least partially explain why I was seeing so little impact here. |
|
Postponing the remaining tasks here to 2.7 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This umbrella issue tracks the progression of the BV theory reasoning. Please add related issue here and what we plan to improve in the future.
bvnotreasoning, see BV: Handle negation natively #800 and [bitv] Add support for (bvnot) in the solver #856.bvand,bvor,bvxor, etc (see feat(BV): Word-level propagation for BV logic #944)(bvand (concat a b) (concat c d))to(concat (bvand a c) (bvand b d)))bv2natandint2bvThe text was updated successfully, but these errors were encountered: