Make sine solver sound with respect to region boundaries (#8117)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 24 Feb 2022 19:08:07 +0000 (13:08 -0600)
committerGitHub <noreply@github.com>
Thu, 24 Feb 2022 19:08:07 +0000 (19:08 +0000)
commit4bba39f1b52210c7a31b8e7542df9dc15b9700c1
treeb1f35557e5d49eebadeafa0e24e26f65866418f9
parent4972960da74afd20fdae8fbb2ca49412866bd9c0
Make sine solver sound with respect to region boundaries (#8117)

Fixes the last benchmark on #7948.

Fixes a refutation soundness issue in the transcendental solver where a concavity region would be incorrectly assigned to a point if it was between the current model value of c*PI and its true value, where c in {-1, -1/2, 1/2, 1}.

We now only assign a concavity region if the model value of the argument lies within sound lower/upper bounds for the boundaries.

Notice that this means that points may be unassignable to a region if they lie inside the approximation interval for c*PI. An application of sin applied to an argument whose model value is that point cannot be refined.

A followup PR will address termination issues where the Taylor degree is incremented even when no function can be refined.
src/theory/arith/nl/transcendental/sine_solver.cpp
src/theory/arith/nl/transcendental/transcendental_solver.cpp
test/regress/CMakeLists.txt
test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 [new file with mode: 0644]