CP: Support for domains on non-leaves #1044
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
bclement-ocp
force-pushed
the
domains_noleaves
branch
2 times, most recently
from
31c1529
to
9c353f3
Compare
bclement-ocp
force-pushed
the
domains_noleaves
branch
from
9c353f3
to
a1e8c7b
Compare
This was referenced Mar 13, 2024
This patch re-adds support for storing domains associated with arbitrary semantic values rather than only with leaves. In a way, it partially reverts OCamlPro#1004 because some domains are not inherently structural and cannot be stored on leaves only (for instance, we want to support interval domains for bit-vectors, but constraints on a concatenation cannot be propagated exactly on the elements of the concatenation). Domains at leaves and non-leaves are connected through _structural propagation_: when the domain of a leaf changes, the change is propagated to the domain of the non-leaves that contains it using the `map_leaves` function; when the domain of a non-leaf changes, the change is propagated to the domain of the leaves it contains using the `fold_leaves` function.
bclement-ocp
force-pushed
the
domains_noleaves
branch
from
a1e8c7b
to
2174392
Compare
Halbaroth
approved these changes
Mar 19, 2024
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jun 14, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jun 20, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jun 20, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jun 20, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jun 20, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jun 21, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 1, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 9, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 16, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 17, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 19, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 19, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 24, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 29, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Jul 30, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Aug 1, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this pull request
Aug 2, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting OCamlPro#1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in OCamlPro#1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
that referenced
this pull request
Aug 6, 2024
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]). This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations. Note that this patch is not reverting #1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in #1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y]. The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
bclement-ocp
added a commit
to bclement-ocp/opam-repository
that referenced
this pull request
Sep 24, 2024
CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)
tjammer
pushed a commit
to tjammer/opam-repository
that referenced
this pull request
Sep 24, 2024
CHANGES: ### Command-line interface - Enable FPA theory by default (OCamlPro/alt-ergo#1177) - Remove deprecated output channels (OCamlPro/alt-ergo#782) - Deprecate the --use-underscore since it produces models that are not SMT-LIB compliant (OCamlPro/alt-ergo#805) - Add --dump-models-on to dump models on a specific output channel (OCamlPro/alt-ergo#838) - Use consistent return codes (OCamlPro/alt-ergo#842) - Add --continue-on-error flag to set the SMT-LIB error behavior (OCamlPro/alt-ergo#853) - Make dolmen the default value for the --frontend option (OCamlPro/alt-ergo#857) - Restore functionality to broken `--profiling` option (OCamlPro/alt-ergo#947) - Add bare-bones support for interactive input in SMT-LIB format (OCamlPro/alt-ergo#949) - Less confusing behavior on timeout (OCamlPro/alt-ergo#982, OCamlPro/alt-ergo#984) - Add `--strict` option for SMT-LIB compliant mode (OCamlPro/alt-ergo#916, OCamlPro/alt-ergo#1133) - Deprecate `sum`, `typing` and `warnings` debug flags (OCamlPro/alt-ergo#1204) ### SMT-LIB support - Add support for the many new SMT-LIB commands (OCamlPro/alt-ergo#837, OCamlPro/alt-ergo#848, OCamlPro/alt-ergo#852, OCamlPro/alt-ergo#863, OCamlPro/alt-ergo#911, OCamlPro/alt-ergo#942, OCamlPro/alt-ergo#945, OCamlPro/alt-ergo#961, OCamlPro/alt-ergo#975, OCamlPro/alt-ergo#1069) - Expose the FPA rounding builtin in the SMT-LIB format (OCamlPro/alt-ergo#876, OCamlPro/alt-ergo#1135) - Allow changing the SAT solver using (set-option) (OCamlPro/alt-ergo#880) - Add support for the `:named` attribute (OCamlPro/alt-ergo#957) - Add support for quoted identifiers (OCamlPro/alt-ergo#909, OCamlPro/alt-ergo#972) - Add support for naming lemmas in SMT-LIB syntax (OCamlPro/alt-ergo#1141, OCamlPro/alt-ergo#1143) ### Model generation - Use post-solve SAT environment in model generation, fixing issues where incorrect models were generated (OCamlPro/alt-ergo#789) - Restore support for records in models (OCamlPro/alt-ergo#793) - Use abstract values instead of dummy values in models where the actual value does not matter (OCamlPro/alt-ergo#804, OCamlPro/alt-ergo#835) - Use fresh names for all abstract values to prevent accidental captures (OCamlPro/alt-ergo#811) - Add support for model generation with the default CDCL solver (OCamlPro/alt-ergo#829) - Support model generation for the BV theory (OCamlPro/alt-ergo#841, OCamlPro/alt-ergo#968) - Add support for optimization (MaxSMT / OptiSMT) with lexicographic Int and Real objectives (OCamlPro/alt-ergo#861, OCamlPro/alt-ergo#921) - Add a SMT-LIB printer for expressions (OCamlPro/alt-ergo#952, OCamlPro/alt-ergo#981, OCamlPro/alt-ergo#1082, OCamlPro/alt-ergo#931, OCamlPro/alt-ergo#932) - Ensure models have a value for all constants in the problem (OCamlPro/alt-ergo#1019) - Fix a rare soundness issue with integer constraints when model generation is enabled (OCamlPro/alt-ergo#1025) - Support model generation for the ADT theory (OCamlPro/alt-ergo#1093, OCamlPro/alt-ergo#1153) ### Theory reasoning - Add word-level propagators for the BV theory (OCamlPro/alt-ergo#944, OCamlPro/alt-ergo#1004, OCamlPro/alt-ergo#1007, OCamlPro/alt-ergo#1010, OCamlPro/alt-ergo#1011, OCamlPro/alt-ergo#1012, OCamlPro/alt-ergo#1040, OCamlPro/alt-ergo#1044, OCamlPro/alt-ergo#1054, OCamlPro/alt-ergo#1055, OCamlPro/alt-ergo#1056, OCamlPro/alt-ergo#1057, OCamlPro/alt-ergo#1065, OCamlPro/alt-ergo#1073, OCamlPro/alt-ergo#1144, OCamlPro/alt-ergo#1152) - Add interval domains and arithmetic propagators for the BV theory (OCamlPro/alt-ergo#1058, OCamlPro/alt-ergo#1083, OCamlPro/alt-ergo#1084, OCamlPro/alt-ergo#1085) - Native support for bv2nat of bit-vector normal forms (OCamlPro/alt-ergo#1154) - Fix incompleteness issues in the BV solver (OCamlPro/alt-ergo#978, OCamlPro/alt-ergo#979) - Abstract more arguments of AC symbols to avoid infinite loops when they contain other AC symbols (OCamlPro/alt-ergo#990) - Do not make irrelevant decisions in CDCL solver, improving performance slightly (OCamlPro/alt-ergo#1041) - Rewrite the ADT theory to use domains and integrate the enum theory into the ADT theory (OCamlPro/alt-ergo#1078, OCamlPro/alt-ergo#1086, OCamlPro/alt-ergo#1087, OCamlPro/alt-ergo#1091, OCamlPro/alt-ergo#1094, OCamlPro/alt-ergo#1138) - Rewrite the Intervals module entirely (OCamlPro/alt-ergo#1108) - Add maximize/minimize terms for matching (OCamlPro/alt-ergo#1166) - Internalize `sign_extend` and `repeat` (OCamlPro/alt-ergo#1192) - Run cross-propagators to completion (OCamlPro/alt-ergo#1221) - Support binary distinct on arbitrary bit-widths (OCamlPro/alt-ergo#1222) - Only perform optimization when building a model (OCamlPro/alt-ergo#1224) - Make sure domains do not overflow the default domain (OCamlPro/alt-ergo#1225) - Do not build unnormalized values in `zero_extend` (OCamlPro/alt-ergo#1226) ### Internal/library changes - Rewrite the Vec module (OCamlPro/alt-ergo#607) - Move printer definitions closer to type definitions (OCamlPro/alt-ergo#808) - Mark proxy names as reserved (OCamlPro/alt-ergo#836) - Use a Zarith-based representation for numbers and bit-vectors (OCamlPro/alt-ergo#850, OCamlPro/alt-ergo#943) - Add native support for (bvnot) in the BV solver (OCamlPro/alt-ergo#856) - Add constant propagators for partially interpreted functions (OCamlPro/alt-ergo#869) - Remove `Util.failwith` in favor of `Fmt.failwith` (OCamlPro/alt-ergo#872) - Add more `Expr` smart constructors (OCamlPro/alt-ergo#877, OCamlPro/alt-ergo#878) - Do not use existential variables for integer division (OCamlPro/alt-ergo#881) - Preserve `Subst` literals to prevent accidental incompleteness (OCamlPro/alt-ergo#886) - Properly start timers (OCamlPro/alt-ergo#924) - Compute a concrete representation of a model instead of performing (OCamlPro/alt-ergo#925) - Allow direct access to the SAT API in the Alt-Ergo library computations during printing (OCamlPro/alt-ergo#927) - Better handling for step limit (OCamlPro/alt-ergo#936) - Add a generic option manager to deal with the dolmen state (OCamlPro/alt-ergo#951) - Expose an imperative SAT API in the Alt-Ergo library (OCamlPro/alt-ergo#962) - Keep track of the SMT-LIB mode (OCamlPro/alt-ergo#971) - Add ability to decide on semantic literals (OCamlPro/alt-ergo#1027, OCamlPro/alt-ergo#1118) - Preserve trigger order when parsing quantifiers with multiple trigger (OCamlPro/alt-ergo#1046). - Store domains inside the union-find module (OCamlPro/alt-ergo#1119) - Remove some polymorphic hashtables (OCamlPro/alt-ergo#1219) ### Build and integration - Drop support for OCaml <4.08.1 (OCamlPro/alt-ergo#803) - Use dune-site for the inequalities plugins. External pluginsm ust now be registered through the dune-site plugin mechanism in the `(alt-ergo plugins)` site to be picked up by Alt-Ergo (OCamlPro/alt-ergo#1049). - Add a release workflow (OCamlPro/alt-ergo#827) - Add a Windows workflow (OCamlPro/alt-ergo#1203) - Mark the dune.inc file as linguist-generated to avoid huge diffs (OCamlPro/alt-ergo#830) - Use GitHub Actions badges in the README (OCamlPro/alt-ergo#882) - Use `dune build @check` to build the project (OCamlPro/alt-ergo#887) - Enable warnings as errors on the CI (OCamlPro/alt-ergo#888) - Uniformization of internal identifiers generation (OCamlPro/alt-ergo#905, OCamlPro/alt-ergo#918) - Use an efficient `String.starts_with` implementation (OCamlPro/alt-ergo#912) - Fix the Makefile (OCamlPro/alt-ergo#914) - Add `Logs` dependency (OCamlPro/alt-ergo#1206) - Use `dynamic_include` to include the generated file `dune.inc` (OCamlPro/alt-ergo#1199) - Support Windows (OCamlPro/alt-ergo#1184,OCamlPro/alt-ergo#1189,OCamlPro/alt-ergo#1195,OCamlPro/alt-ergo#1199,OCamlPro/alt-ergo#1200) - Wrap the library `Alt_ergo_prelude` (OCamlPro/alt-ergo#1223) ### Testing - Use --enable-assertions in tests (OCamlPro/alt-ergo#809) - Add a test for push/pop (OCamlPro/alt-ergo#843) - Use the CDCL solver when testing model generation (OCamlPro/alt-ergo#938) - Do not test .smt2 files with the legacy frontend (OCamlPro/alt-ergo#939) - Restore automatic creation of .expected files (OCamlPro/alt-ergo#941) ### Documentation - Add a new example for model generation (OCamlPro/alt-ergo#826) - Add a Pygments lexer for the Alt-Ergo native language (OCamlPro/alt-ergo#862) - Update the current authors (OCamlPro/alt-ergo#865) - Documentation of the `Enum` theory (OCamlPro/alt-ergo#871) - Document `Th_util.lit_origin` (OCamlPro/alt-ergo#915) - Document the CDCL-Tableaux solver (OCamlPro/alt-ergo#995) - Document Windows support (OCamlPro/alt-ergo#1216) - Remove instructions to install Alt-Ergo on Debian (OCamlPro/alt-ergo#1217) - Document optimization feature (OCamlPro/alt-ergo#1231)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This patch re-adds support for storing domains associated with arbitrary
semantic values rather than only with leaves. In a way, it partially
reverts #1004 because some domains are not inherently structural and
cannot be stored on leaves only (for instance, we want to support
interval domains for bit-vectors, but constraints on a concatenation
cannot be propagated exactly on the elements of the concatenation).
Domains at leaves and non-leaves are connected through structural
propagation: when the domain of a leaf changes, the change is
propagated to the domain of the non-leaves that contains it using the
map_leavesfunction; when the domain of a non-leaf changes, the changeis propagated to the domain of the leaves it contains using the
fold_leavesfunction.