diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-29 17:00:23 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-16 23:23:30 -0700 |
| commit | 9ba1854be7d798a899a2b46c2707d376938c5d18 (patch) | |
| tree | d2a0f5712a7e5e14242036d0460b6ab30b7b44e4 /src/theory/quantifiers/sygus/cegis_unif.cpp | |
| parent | a6bd02c5c442b806b5e01fed40ab9d1017e42bc3 (diff) | |
Add rewrite for splitting equalities
This commit adds an extended rewrite that splits a given string equality
into multiple equalities if it can find prefixes of equal lengths.
For example: `(= (str.++ x "AB" z) (str.++ "A" x y)) ---> (and (=
(str.++ x "A") (str.++ "A" x)) (= (str.++ "B" z) y))`
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis_unif.cpp')
0 files changed, 0 insertions, 0 deletions