Unsoundness in model generation #1022
Assignees
Labels
Comments
|
Minimised with ddSMT (although not actually much simpler): |
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Jan 8, 2024
Model generation for arithmetic constraints proceeds in two stages: - In the first stage, we only choose a value for variables that are within a finite domain (i.e. integer variables bounded from both above and below). This is the behavior of regular case splits, and happens in function `default_case_split`. - In the second stage, which we only reach if model generation is enabled, we must select a value for all variables. In this case, we select one interval for variables that can have multiple intervals (recall that we model arithmetic domains using unions of intervals). This happens in function `case_split_union_of_intervals`. If the selected interval is finite, we go back to the first stage in the next case split. - In the final stage, all remaining variables have infinite intervals as domains, and we must now pick a value for these. This happens in `model_from_unbounded_domains` -- even though for rational variables, the domain can still be bounded. For integers however, infinite intervals mean that they lack either a finite lower or upper bound (or both). For integers, we create a new simplex environment in `fm_simplex_unbounded_integers_encoding` where we adjust the bounds by a factor of half the sum of the absolute values of the coefficients. This means that an inequality `0 < 3x + 4y` becomes `0 + (3 + 4) / 2 < 3x + 4y`, i.e. `3.5 < 3x + 4y`. This removes `x = 1, y = 0` from the domain. On its own, this would be correct (albeit strange) because after removing a finite number of elements from an infinite domain there is still an infinite number of elements to choose from. But within a larger system this can (and is) problematic. This patch removes the "adjustment" of the bounds which is not justified and actually causes unsoundness. Fixes OCamlPro#1022 Co-Authored-By: Guillaume Bury <guillaume.bury@gmail.com>
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Jan 9, 2024
Model generation for arithmetic constraints proceeds in two stages: - In the first stage, we only choose a value for variables that are within a finite domain (i.e. integer variables bounded from both above and below). This is the behavior of regular case splits, and happens in function `default_case_split`. - In the second stage, which we only reach if model generation is enabled, we must select a value for all variables. In this case, we select one interval for variables that can have multiple intervals (recall that we model arithmetic domains using unions of intervals). This happens in function `case_split_union_of_intervals`. If the selected interval is finite, we go back to the first stage in the next case split. - In the final stage, all remaining variables have infinite intervals as domains, and we must now pick a value for these. This happens in `model_from_unbounded_domains` -- even though for rational variables, the domain can still be bounded. For integers however, infinite intervals mean that they lack either a finite lower or upper bound (or both). For integers, we create a new simplex environment in `fm_simplex_unbounded_integers_encoding` where we adjust the bounds by a factor of half the sum of the absolute values of the coefficients. This means that an inequality `0 < 3x + 4y` becomes `0 + (3 + 4) / 2 < 3x + 4y`, i.e. `3.5 < 3x + 4y`. This removes `x = 1, y = 0` from the domain. On its own, this would be correct (albeit strange) because after removing a finite number of elements from an infinite domain there is still an infinite number of elements to choose from. But within a larger system this can (and is) problematic. This patch removes the "adjustment" of the bounds which is not justified and actually causes unsoundness. Fixes OCamlPro#1022 Co-Authored-By: Guillaume Bury <guillaume.bury@gmail.com>
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Jan 9, 2024
Model generation for arithmetic constraints proceeds in two stages: - In the first stage, we only choose a value for variables that are within a finite domain (i.e. integer variables bounded from both above and below). This is the behavior of regular case splits, and happens in function `default_case_split`. - In the second stage, which we only reach if model generation is enabled, we must select a value for all variables. In this case, we select one interval for variables that can have multiple intervals (recall that we model arithmetic domains using unions of intervals). This happens in function `case_split_union_of_intervals`. If the selected interval is finite, we go back to the first stage in the next case split. - In the final stage, all remaining variables have infinite intervals as domains, and we must now pick a value for these. This happens in `model_from_unbounded_domains` -- even though for rational variables, the domain can still be bounded. For integers however, infinite intervals mean that they lack either a finite lower or upper bound (or both). For integers, we create a new simplex environment in `fm_simplex_unbounded_integers_encoding` where we adjust the bounds by a factor of half the sum of the absolute values of the coefficients. This means that an inequality `0 < 3x + 4y` becomes `0 + (3 + 4) / 2 < 3x + 4y`, i.e. `3.5 < 3x + 4y`. This removes `x = 1, y = 0` from the domain. On its own, this would be correct (albeit strange) because after removing a finite number of elements from an infinite domain there is still an infinite number of elements to choose from. But within a larger system this can (and is) problematic. This patch removes the "adjustment" of the bounds which is not justified and actually causes unsoundness. Fixes OCamlPro#1022 Co-Authored-By: Guillaume Bury <guillaume.bury@gmail.com>
bclement-ocp
added a commit
to bclement-ocp/alt-ergo
that referenced
this issue
Jan 9, 2024
Model generation for arithmetic constraints proceeds in two stages: - In the first stage, we only choose a value for variables that are within a finite domain (i.e. integer variables bounded from both above and below). This is the behavior of regular case splits, and happens in function `default_case_split`. - In the second stage, which we only reach if model generation is enabled, we must select a value for all variables. In this case, we select one interval for variables that can have multiple intervals (recall that we model arithmetic domains using unions of intervals). This happens in function `case_split_union_of_intervals`. If the selected interval is finite, we go back to the first stage in the next case split. - In the final stage, all remaining variables have infinite intervals as domains, and we must now pick a value for these. This happens in `model_from_unbounded_domains` -- even though for rational variables, the domain can still be bounded. For integers however, infinite intervals mean that they lack either a finite lower or upper bound (or both). For integers, we create a new simplex environment in `fm_simplex_unbounded_integers_encoding` where we adjust the bounds by a factor of half the sum of the absolute values of the coefficients. This means that an inequality `0 < 3x + 4y` becomes `0 + (3 + 4) / 2 < 3x + 4y`, i.e. `3.5 < 3x + 4y`. This removes `x = 1, y = 0` from the domain. On its own, this would be correct (albeit strange) because after removing a finite number of elements from an infinite domain there is still an infinite number of elements to choose from. But within a larger system this can (and is) problematic. This patch removes the "adjustment" of the bounds which is not justified and actually causes unsoundness. Fixes OCamlPro#1022 Co-Authored-By: Guillaume Bury <guillaume.bury@gmail.com>
Halbaroth
pushed a commit
that referenced
this issue
Jan 9, 2024
Model generation for arithmetic constraints proceeds in two stages: - In the first stage, we only choose a value for variables that are within a finite domain (i.e. integer variables bounded from both above and below). This is the behavior of regular case splits, and happens in function `default_case_split`. - In the second stage, which we only reach if model generation is enabled, we must select a value for all variables. In this case, we select one interval for variables that can have multiple intervals (recall that we model arithmetic domains using unions of intervals). This happens in function `case_split_union_of_intervals`. If the selected interval is finite, we go back to the first stage in the next case split. - In the final stage, all remaining variables have infinite intervals as domains, and we must now pick a value for these. This happens in `model_from_unbounded_domains` -- even though for rational variables, the domain can still be bounded. For integers however, infinite intervals mean that they lack either a finite lower or upper bound (or both). For integers, we create a new simplex environment in `fm_simplex_unbounded_integers_encoding` where we adjust the bounds by a factor of half the sum of the absolute values of the coefficients. This means that an inequality `0 < 3x + 4y` becomes `0 + (3 + 4) / 2 < 3x + 4y`, i.e. `3.5 < 3x + 4y`. This removes `x = 1, y = 0` from the domain. On its own, this would be correct (albeit strange) because after removing a finite number of elements from an infinite domain there is still an infinite number of elements to choose from. But within a larger system this can (and is) problematic. This patch removes the "adjustment" of the bounds which is not justified and actually causes unsoundness. Fixes #1022 Co-authored-by: Guillaume Bury <guillaume.bury@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
On the following sat problem from the SMT-LIB (QF_LIA/20180326-Bromberger/unbd-sage/unbd010v15c/unbd-sage0):
Alt-Ergo replies:
That's good (the problem is SAT).
If we request model generation, however, we have an issue:
Some more info:
QF_LIA/20180326-Bromberger/unbd-sageand other SAT problems with integers (e.g.QF_LIA/dilig/15-17.smt2).model_from_simplexint_simenvironment we create with "FM-Simplex encoding" (I do not know what that is) here is actually unsatenv.int_simhere works, at least in this specific case, but presumably that is not acceptable to use in the general case (?). I do not know why we need this "FM-Simplex" encoding (yet), but it seems that we are computing it wrong, somehow.The text was updated successfully, but these errors were encountered: