diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-17 11:26:32 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-17 11:26:32 -0500 |
| commit | c752258539ddb4c97b4fcbe7481cb1151ad182d0 (patch) | |
| tree | faf7a72b076f5c9e498c6522e06be76b5a7468c4 /test | |
| parent | 5915a62d767dd8a33dd13be7c6545c6553442878 (diff) | |
Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)
Fixes #4620.
The extended rewrite (and A B) ---> (and A (B * { A -> true } ) triggers an unsoundness when B contains witness terms. More generally, contextual substitution into witness terms is unsound since the skolemization of witness terms is added globally whereas the substitution corresponds to a fact that holds locally. This means that A -> true above may be added as a global constraint indirectly through witness skolemization.
A general example of this unsoundness:
(or (and (>= x 0) (P (witness ((z Int)) (=> (>= x 0) (= (* z z) x))))) F)
rewrites to
(or (and (>= x 0) (P (witness ((z Int)) (= (* z z) x)))) F)
preprocesses to
(and (or (and (>= x 0) (P k)) F) (= (* k k) x))
which now implies that (>= x 0) by the last conjunct, whereas this was not implied in the original formula
This PR limits the kinds that can be traversed when applying substitutions in the extended rewriter, including from the rewrite above. In particular, the fix ensures that the partialSubstitute method is used in the extended rewriter when applicable, which now explicitly disallows recursion on WITNESS.
Notice that this fixes contextual substitutions in the extended rewriter, but does not fix the more general issue. In particular, we still should be careful to check if contextual substitutions are applied by any other preprocessing passes.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/ext-rew-test.smt2 | 1 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2 | 5 |
3 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 93d6a3ef8..cdac5fc6c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1549,6 +1549,7 @@ set(regress_1_tests regress1/quantifiers/issue4062-cegqi-aux.smt2 regress1/quantifiers/issue4243-prereg-inc.smt2 regress1/quantifiers/issue4290-cegqi-r.smt2 + regress1/quantifiers/issue4620-erq-witness-unsound.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lra-vts-inf.smt2 diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2 index 3fb3a9e53..726487e18 100644 --- a/test/regress/regress0/fp/ext-rew-test.smt2 +++ b/test/regress/regress0/fp/ext-rew-test.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: symfpu ; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg ; EXPECT: unsat (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2 b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2 new file mode 100644 index 000000000..ee7cafd63 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue4620-erq-witness-unsound.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --ext-rewrite-quant +; EXPECT: sat +(set-logic NIA) +(assert (exists ((x Int)) (= (div 1 x x) x))) +(check-sat) |