Fix infinite loop in arith_ite_simp (#4805)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Wed, 12 Aug 2020 13:17:18 +0000 (15:17 +0200)
committerGitHub <noreply@github.com>
Wed, 12 Aug 2020 13:17:18 +0000 (08:17 -0500)
commit558ceb2f64877fa2cc5f1cd448147e529b5c1c02
tree31beed1c4b0b792bf6328b25a5e576e48b118970
parent0e39025474cb32a3b96ebc93afd8a761ca0ec9ef
Fix infinite loop in arith_ite_simp (#4805)

We have an open issue with an infinite loop with --ite-simp for a long time in #789 , for example on

(declare-fun a () Int)
(declare-fun b () Int)
(assert
    (and
        (= 1 (+ a b))
        (or (= 0 a) (= 0 b))
        (or (= 0 b) (>= b 8))
        (or (= 0 a) (not (>= b 8)))
    )
)
(check-sat)
The problem goes back to arith_ite_utils.cpp and roughly is as follows:
The method solveBinOr looks for patterns like (or (= b 0) (= b 1)). It introduces a new Boolean variable deor_1 and substitutes b -> (ite deor_1 1 0).
The method also stores another mapping in d_skolems: deor_1 -> (>= b 8) here which is also used in selectForCmp. However, these skolems are also used to add even more substitutions here after applying the already added substitutions to it. Eventually, we have a substitution deor_1 -> (>= (ite deor_1 1 0) 8) which inevitably leads to an infinite loop.
I have found no reason for the second mapping (deor_1 -> (>= b 8)) to be added as a substitution, and thus this PR removes it.

Benchmarks are running to check whether there are further issues with this, and whether this simplification is beneficial.

Fixes #789.
src/theory/arith/arith_ite_utils.cpp
src/theory/arith/arith_ite_utils.h