From 926fa8e8dbb6d593f17afdca63c48aea76248b26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <basile.clement@ocamlpro.com>
Date: Mon, 8 Jan 2024 13:57:37 +0100
Subject: [PATCH] fix(arith): Do not overly tighten bounds over infinite
domains
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>
---
src/lib/reasoners/intervalCalculus.ml | 36 +++++++--------------------
tests/dune.inc | 23 ++++++++++++++++-
tests/issues/1022.models.expected | 13 ++++++++++
tests/issues/1022.models.smt2 | 24 ++++++++++++++++++
tests/issues/777.models.expected | 2 +-
tests/models/uf/uf2.models.expected | 4 +--
6 files changed, 71 insertions(+), 31 deletions(-)
create mode 100644 tests/issues/1022.models.expected
create mode 100644 tests/issues/1022.models.smt2
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index 3f9b161e01..bd74f7b766 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -1921,37 +1921,19 @@ let fm_simplex_unbounded_integers_encoding env uf =
"case-split over unions of intervals is needed !!!";
assert false
- | [(mn, ex_mn), (mx, ex_mx)] ->
+ | [(lb, ex_lb), (ub, ex_ub)] ->
let l, c = P.to_list p in
- let l = List.rev_map (fun (c, x) -> x, c) (List.rev l) in
- assert (Q.sign c = 0);
- let cst0 =
- List.fold_left (fun z (_, c) -> Q.add z (Q.abs c))Q.zero l
- in
- let cst = Q.div cst0 (Q.from_int 2) in
- assert (mn == None || mx == None);
- let min =
- let mn =
- match mn with
- | None -> None
- | Some (q, q') -> Some (Q.add q cst, q')
- in
- bnd_to_simplex_bound (mn, ex_mn)
- in
- let max =
- let mx =
- match mx with
- | None -> None
- | Some (q, q') -> Some (Q.sub q cst, q')
- in
- bnd_to_simplex_bound (mx, ex_mx)
- in
+ assert (Q.is_zero c);
+ assert (lb == None || ub == None);
+ let min = bnd_to_simplex_bound (lb, ex_lb) in
+ let max = bnd_to_simplex_bound (ub, ex_ub) in
match l with
| [] -> assert false
- | [x, c] ->
+ | [c, x] ->
assert (Q.is_one c);
Sim.Assert.var simplex x ?min ?max |> fst
| _ ->
+ let l = List.rev_map (fun (c, x) -> x, c) (List.rev l) in
let xp = alien_of p in
let sim_p =
match Sim.Core.poly_of_slake simplex xp with
@@ -2009,7 +1991,7 @@ let model_from_simplex sim is_int env uf =
)[] (List.rev main_vars)
-let model_from_unbounded_domains =
+let model_from_infinite_domains =
let mk_cs acc (x, v, _ex) =
((LR.view (LR.mk_eq x v)), true,
Th_util.CS (Th_util.Th_arith, Q.from_int 2)) :: acc
@@ -2040,7 +2022,7 @@ let case_split env uf ~for_model =
else
begin
match case_split_union_of_intervals env uf with
- | [] -> model_from_unbounded_domains env uf
+ | [] -> model_from_infinite_domains env uf
| l -> l
end
| _ -> res
diff --git a/tests/dune.inc b/tests/dune.inc
index 26d82ad68c..3224bab3ee 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -193838,7 +193838,28 @@
(alias runtest-quick)
(package alt-ergo)
(action
- (diff 340.expected 340_fpa.output))))
+ (diff 340.expected 340_fpa.output)))
+ (rule
+ (target 1022.models_dolmen.output)
+ (deps (:input 1022.models.smt2))
+ (package alt-ergo)
+ (action
+ (chdir %{workspace_root}
+ (with-stdout-to %{target}
+ (ignore-stderr
+ (with-accepted-exit-codes (or 0)
+ (run %{bin:alt-ergo}
+ --timelimit=2
+ --enable-assertions
+ --output=smtlib2
+ --frontend dolmen
+ %{input})))))))
+ (rule
+ (deps 1022.models_dolmen.output)
+ (alias runtest-quick)
+ (package alt-ergo)
+ (action
+ (diff 1022.models.expected 1022.models_dolmen.output))))
; Auto-generated part end
; File auto-generated by gentests
diff --git a/tests/issues/1022.models.expected b/tests/issues/1022.models.expected
new file mode 100644
index 0000000000..c1f647bc74
--- /dev/null
+++ b/tests/issues/1022.models.expected
@@ -0,0 +1,13 @@
+
+unknown
+(
+ (define-fun x () Int 3)
+ (define-fun x1 () Int (- 3))
+ (define-fun x2 () Int (- 2))
+ (define-fun x3 () Int 0)
+ (define-fun x4 () Int (- 1))
+ (define-fun x5 () Int 2)
+ (define-fun x6 () Int 0)
+ (define-fun x7 () Int 0)
+ (define-fun x9 () Int 2)
+)
diff --git a/tests/issues/1022.models.smt2 b/tests/issues/1022.models.smt2
new file mode 100644
index 0000000000..02a8316d1b
--- /dev/null
+++ b/tests/issues/1022.models.smt2
@@ -0,0 +1,24 @@
+(set-option :produce-models true)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(declare-fun x5 () Int)
+(declare-fun x6 () Int)
+(declare-fun x7 () Int)
+(declare-fun x9 () Int)
+(assert (and
+(< 0 x)
+(< 0 (+ x x2))
+(< 0 (+ x4 x9))
+(< 0 (+ x5 x6))
+(< 0 (* x1 (- 1)))
+(< 1 (+ x3 x5 x9 x2))
+(< 1 (+ x5 (* x3 (- 1))))
+(< 0 (+ x2 (* 27 x7) (* x3 (- 1)) (* x4 (- 26))))
+(< 0 (+ x3 x6 (* 9 x7) (* x1 (- 1)) (* x2 (- 7)) (* x4 (- 14)) (* x5 (- 15))))
+(< (- 39) (+ (* x (- 7)) (* 7 x1) (* 2 x2) (* 18 x4) (* 14 x5) (* x6 (- 3)) (* x7 (- 12)) (* x9 (- 1))))))
+(check-sat)
+(get-model)
diff --git a/tests/issues/777.models.expected b/tests/issues/777.models.expected
index 1a34774938..8d04d7d4b3 100644
--- a/tests/issues/777.models.expected
+++ b/tests/issues/777.models.expected
@@ -1,5 +1,5 @@
unknown
(
- (define-fun i () Int 2)
+ (define-fun i () Int 1)
)
diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected
index ce06fd3336..902676ae79 100644
--- a/tests/models/uf/uf2.models.expected
+++ b/tests/models/uf/uf2.models.expected
@@ -1,7 +1,7 @@
unknown
(
- (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 2)) 0 2))
+ (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 1)) 0 1))
(define-fun a () Int 0)
- (define-fun b () Int (- 2))
+ (define-fun b () Int (- 1))
)