Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

solution unsoundness on a string formula #6483

Closed
zhendongsu opened this issue May 4, 2021 · 0 comments · Fixed by #6562
Closed

solution unsoundness on a string formula #6483

zhendongsu opened this issue May 4, 2021 · 0 comments · Fixed by #6562
Assignees
@4tXJ7f @ajreynol

Comments

@zhendongsu
Copy link

Commit: 441c53b
OS: Ubuntu 18.04

It also affects cvc4-1.7 and cvc4-1.8, but both can detect the produced invalid model.

[619] % z3release small.smt2
unsat
(error "line 14 column 10: model is not available")
[620] % cvc5 -q --strings-exp --produce-models --check-models small.smt2
sat
(
(define-fun a () String "")
)
[621] % 
[621] % cat small.smt2
(declare-fun a () String)
(assert
 (xor
  (= (= (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B")
      (str.replace "B" (str.replace "B" a (str.++ a "B")) a))
   (not
    (= (str.replace "B" (str.replace a "B" "") "B")
     (str.replace "B" a (str.++ a "B")))))
  (= (str.replace "B" a "")
   (str.replace "B" a
    (ite (not (= (str.replace "" (str.replace a "" a) "") "")) ""
     (str.replace "" (str.replace a "B" "") "B"))))))
(check-sat)
(get-model)
[622] %
@ajreynol ajreynol self-assigned this May 4, 2021
@4tXJ7f 4tXJ7f self-assigned this May 18, 2021
4tXJ7f added a commit to 4tXJ7f/cvc5 that referenced this issue May 18, 2021
@4tXJ7f
Fix collectEmptyEqs() in string utils
c2faac7 
Fixes cvc5#6483. The benchmark in the issue was performing the following
incorrect rewrite:

```
 Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
```

The rewrite `RPL_X_Y_X_SIMP` rewrites terms of the form `(str.replace x
y x)`, where `x` is of length one and `(= y "")` rewrites to a
conjunction of equalities of the form `(= y_i "")` where `y_i` is some
term. The function responsible for collecting the terms `y_i` from this
conjunction, `collectEmptyEqs()`, returns a `bool` and a vector of
`Node`s. The `bool` indicates whether all equalities in the conjunction
were of the form `(= y_i "")`. The rewrite `RPL_X_Y_X_SIMP` only applies
if this is true. However, `collectEmptyEqs()` had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
`collectEmptyEqs()` and adds tests.
@4tXJ7f 4tXJ7f mentioned this issue May 18, 2021
Merged
ajreynol pushed a commit that referenced this issue May 18, 2021
@4tXJ7f
Fix collectEmptyEqs() in string utils (#6562)
c214051 
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:

 Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
The rewrite RPL_X_Y_X_SIMP rewrites terms of the form (str.replace x y x), where x is of length one and (= y "") rewrites to a
conjunction of equalities of the form (= y_i "") where y_i is some
term. The function responsible for collecting the terms y_i from this
conjunction, collectEmptyEqs(), returns a bool and a vector of
Nodes. The bool indicates whether all equalities in the conjunction
were of the form (= y_i ""). The rewrite RPL_X_Y_X_SIMP only applies
if this is true. However, collectEmptyEqs() had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs() and adds tests.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@4tXJ7f 4tXJ7f

@ajreynol ajreynol

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix collectEmptyEqs() in string utils 4tXJ7f/cvc5
3 participants
@4tXJ7f @ajreynol @zhendongsu