diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-15 14:08:03 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-15 19:08:03 +0000 |
commit | 216f3c9fb07a08909942b91a2a4739cd178f5a72 (patch) | |
tree | 00de2d826d1b4ad6124856536923a2463c4d8641 /test/regress | |
parent | 6cbb7824dabd7ab8e85472a22ba30ad2498afebc (diff) |
Make nonlinear extension account for relevant term set (#6147)
This fixes a subtle issue with non-linear and theory combination.
It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.
In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.
Fixes #5662.
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress1/nl/issue5662-nl-tc-min.smt2 | 16 | ||||
-rw-r--r-- | test/regress/regress1/nl/issue5662-nl-tc.smt2 | 17 |
3 files changed, 35 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 30cdf43d9..5c28a34cc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1596,6 +1596,8 @@ set(regress_1_tests regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 regress1/nl/issue5372-2-no-m-presolve.smt2 + regress1/nl/issue5662-nl-tc.smt2 + regress1/nl/issue5662-nl-tc-min.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 regress1/nl/metitarski_3_4_2e.smt2 diff --git a/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 new file mode 100644 index 000000000..0e7279ef9 --- /dev/null +++ b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 @@ -0,0 +1,16 @@ +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun j () Real) +(declare-fun k () Real) +(declare-fun h () Real) +(assert (< 0 k)) +(assert (= 1 (* k j))) +(assert + (or + (= h 0) + (= 0.0 (* a k)) + ) +) +(assert (distinct a h)) +(check-sat) diff --git a/test/regress/regress1/nl/issue5662-nl-tc.smt2 b/test/regress/regress1/nl/issue5662-nl-tc.smt2 new file mode 100644 index 000000000..d805b721d --- /dev/null +++ b/test/regress/regress1/nl/issue5662-nl-tc.smt2 @@ -0,0 +1,17 @@ +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(declare-fun d () Real) +(declare-fun j () Real) +(declare-fun e () Real) +(declare-fun f () Real) +(declare-fun k () Real) +(declare-fun g () Real) +(declare-fun h () Real) +(assert (forall ((i Real)) (xor (and (or (and (or (and (or (and (or + (and (> 0.0 (* a e) (* c e)) (>= 0 k)) (<= g 0)) (= (* b j) + 2.0))))) (> f k)) (>= 0.0 k))) (>= 0 k)))) +(assert (distinct a (* d h))) +(check-sat) |