diff --git a/benchmarks/instance08175.smt2 b/benchmarks/instance08175.smt2 new file mode 100644 index 000000000..fe34ad2d5 --- /dev/null +++ b/benchmarks/instance08175.smt2 @@ -0,0 +1,23 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (re.* (str.to_re " ")) (str.to_re "=") (re.* (str.to_re " ")) (re.* (str.to_re "\u{22}")) (str.to_re "cid") (re.* (str.to_re " ")) (str.to_re ":") (re.* (str.to_re " ")) (re.+ (re.union (str.to_re "\u{22}") (str.to_re "<") (str.to_re ">") (str.to_re " "))) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.++ ((_ re.loop 1 11) (re.union (re.range "a" "z") (re.range "0" "9"))) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.++ ((_ re.loop 3 3) (re.range "0" "9")) ((_ re.loop 1 1) (re.union (str.to_re "-") (str.to_re "|") (str.to_re "/"))) ((_ re.loop 6 6) (re.range "0" "9")) ((_ re.loop 1 1) (re.union (str.to_re "-") (str.to_re "|") (str.to_re "/"))) ((_ re.loop 6 6) (re.range "0" "9")) (str.to_re "\u{a}")))) +(assert (not (str.in_re X (str.to_re "http://tv.seekmo.com/showme.aspx?keyword=\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "@") (re.union (re.++ ((_ re.loop 2 255) (re.union (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9") (str.to_re "-"))) (str.to_re ".") (re.union (str.to_re "ad") (str.to_re "ae") (str.to_re "af") (str.to_re "ag") (str.to_re "ai") (str.to_re "al") (str.to_re "am") (str.to_re "an") (str.to_re "ao") (str.to_re "aq") (str.to_re "ar") (str.to_re "as") (str.to_re "at") (str.to_re "au") (str.to_re "aw") (str.to_re "az") (str.to_re "ba") (str.to_re "bb") (str.to_re "bd") (str.to_re "be") (str.to_re "bf") (str.to_re "bg") (str.to_re "bh") (str.to_re "bi") (str.to_re "bj") (str.to_re "bm") (str.to_re "bn") (str.to_re "bo") (str.to_re "br") (str.to_re "bs") (str.to_re "bt") (str.to_re "bv") (str.to_re "bw") (str.to_re "by") (str.to_re "bz") (str.to_re "ca") (str.to_re "cc") (str.to_re "cf") (str.to_re "cg") (str.to_re "ch") (str.to_re "ci") (str.to_re "ck") (str.to_re "cl") (str.to_re "cm") (str.to_re "cn") (str.to_re "co") (str.to_re "cr") (str.to_re "cu") (str.to_re "cv") (str.to_re "cx") (str.to_re "cy") (str.to_re "cz") (str.to_re "de") (str.to_re "di") (str.to_re "dk") (str.to_re "dm") (str.to_re "do") (str.to_re "dz") (str.to_re "ec") (str.to_re "ee") (str.to_re "eg") (str.to_re "eh") (str.to_re "er") (str.to_re "es") (str.to_re "et") (str.to_re "fi") (str.to_re "fj") (str.to_re "fk") (str.to_re "fm") (str.to_re "fo") (str.to_re "fr") (str.to_re "ga") (str.to_re "gb") (str.to_re "gd") (str.to_re "ge") (str.to_re "gf") (str.to_re "gh") (str.to_re "gi") (str.to_re "gl") (str.to_re "gm") (str.to_re "gn") (str.to_re "gp") (str.to_re "gq") (str.to_re "gr") (str.to_re "gs") (str.to_re "gt") (str.to_re "gu") (str.to_re "gw") (str.to_re "gy") (str.to_re "hk") (str.to_re "hm") (str.to_re "hn") (str.to_re "hr") (str.to_re "ht") (str.to_re "hu") (str.to_re "id") (str.to_re "ie") (str.to_re "il") (str.to_re "in") (str.to_re "io") (str.to_re "iq") (str.to_re "ir") (str.to_re "is") (str.to_re "it") (str.to_re "jo") (str.to_re "jm") (str.to_re "jp") (str.to_re "ke") (str.to_re "kg") (str.to_re "kh") (str.to_re "ki") (str.to_re "km") (str.to_re "kn") (str.to_re "kp") (str.to_re "kr") (str.to_re "kw") (str.to_re "ky") (str.to_re "kz") (str.to_re "la") (str.to_re "lb") (str.to_re "lc") (str.to_re "li") (str.to_re "lk") (str.to_re "lr") (str.to_re "ls") (str.to_re "lt") (str.to_re "lu") (str.to_re "lv") (str.to_re "ly") (str.to_re "ma") (str.to_re "mc") (str.to_re "md") (str.to_re "mg") (str.to_re "mh") (str.to_re "mk") (str.to_re "ml") (str.to_re "mm") (str.to_re "mn") (str.to_re "mo") (str.to_re "mp") (str.to_re "mq") (str.to_re "mr") (str.to_re "ms") (str.to_re "mt") (str.to_re "mu") (str.to_re "mv") (str.to_re "mw") (str.to_re "mx") (str.to_re "my") (str.to_re "mz") (str.to_re "an") (str.to_re "nc") (str.to_re "ne") (str.to_re "nf") (str.to_re "ng") (str.to_re "ni") (str.to_re "nl") (str.to_re "no") (str.to_re "np") (str.to_re "nr") (str.to_re "nt") (str.to_re "nu") (str.to_re "nz") (str.to_re "om") (str.to_re "pa") (str.to_re "pe") (str.to_re "pf") (str.to_re "pg") (str.to_re "ph") (str.to_re "pk") (str.to_re "pl") (str.to_re "pm") (str.to_re "pn") (str.to_re "pr") (str.to_re "pt") (str.to_re "pw") (str.to_re "py") (str.to_re "qa") (str.to_re "re") (str.to_re "ro") (str.to_re "ru") (str.to_re "rw") (str.to_re "sa") (str.to_re "sb") (str.to_re "sc") (str.to_re "sd") (str.to_re "se") (str.to_re "sq") (str.to_re "sh") (str.to_re "si") (str.to_re "sj") (str.to_re "sk") (str.to_re "sl") (str.to_re "sm") (str.to_re "sn") (str.to_re "so") (str.to_re "sr") (str.to_re "st") (str.to_re "su") (str.to_re "sv") (str.to_re "sy") (str.to_re "sz") (str.to_re "tc") (str.to_re "td") (str.to_re "tf") (str.to_re "tg") (str.to_re "th") (str.to_re "tj") (str.to_re "tk") (str.to_re "tm") (str.to_re "tn") (str.to_re "to") (str.to_re "tp") (str.to_re "tr") (str.to_re "tt") (str.to_re "tv") (str.to_re "tw") (str.to_re "tz") (str.to_re "ua") (str.to_re "ug") (str.to_re "uk") (str.to_re "um") (str.to_re "us") (str.to_re "uy") (str.to_re "uz") (str.to_re "va") (str.to_re "vc") (str.to_re "ve") (str.to_re "vg") (str.to_re "vi") (str.to_re "vn") (str.to_re "vu") (str.to_re "wf") (str.to_re "ws") (str.to_re "ye") (str.to_re "yt") (str.to_re "yu") (str.to_re "za") (str.to_re "zm") (str.to_re "zr") (str.to_re "zw") (str.to_re "arpa") (str.to_re "arts") (str.to_re "biz") (str.to_re "com") (str.to_re "edu") (str.to_re "firm") (str.to_re "gov") (str.to_re "info") (str.to_re "int") (str.to_re "mil") (str.to_re "nato") (str.to_re "net") (str.to_re "nom") (str.to_re "org") (str.to_re "rec") (str.to_re "store") (str.to_re "web"))) (re.++ (re.union (re.++ (str.to_re "25") (re.range "0" "5")) (re.++ (str.to_re "2") (re.range "0" "4") (re.range "0" "9")) (re.++ ((_ re.loop 1 1) (re.range "0" "1")) ((_ re.loop 2 2) (re.range "0" "9"))) (re.++ ((_ re.loop 1 1) (re.range "1" "9")) ((_ re.loop 1 1) (re.range "0" "9"))) (re.range "1" "9")) (str.to_re ".") (re.union (re.++ (str.to_re "25") (re.range "0" "5")) (re.++ (str.to_re "2") (re.range "0" "4") (re.range "0" "9")) (re.++ ((_ re.loop 1 1) (re.range "0" "1")) ((_ re.loop 2 2) (re.range "0" "9"))) (re.++ ((_ re.loop 1 1) (re.range "1" "9")) ((_ re.loop 1 1) (re.range "0" "9"))) (re.range "1" "9") (str.to_re "0")) (str.to_re ".") (re.union (re.++ (str.to_re "25") (re.range "0" "5")) (re.++ (str.to_re "2") (re.range "0" "4") (re.range "0" "9")) (re.++ ((_ re.loop 1 1) (re.range "0" "1")) ((_ re.loop 2 2) (re.range "0" "9"))) (re.++ ((_ re.loop 1 1) (re.range "1" "9")) ((_ re.loop 1 1) (re.range "0" "9"))) (re.range "1" "9") (str.to_re "0")) (str.to_re ".") (re.union (re.++ (str.to_re "25") (re.range "0" "5")) (re.++ (str.to_re "2") (re.range "0" "4") (re.range "0" "9")) (re.++ ((_ re.loop 1 1) (re.range "0" "1")) ((_ re.loop 2 2) (re.range "0" "9"))) (re.++ ((_ re.loop 1 1) (re.range "1" "9")) ((_ re.loop 1 1) (re.range "0" "9"))) (re.range "0" "9")))) (str.to_re "\u{a}") (re.+ (re.union (str.to_re "_") (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9") (str.to_re "-"))) (str.to_re ".") (re.* (re.union (str.to_re "_") (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9") (str.to_re "-")))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance08315.smt2 b/benchmarks/instance08315.smt2 new file mode 100644 index 000000000..45eecdd57 --- /dev/null +++ b/benchmarks/instance08315.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status sat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (str.to_re "\u{a}") (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "3"))) (str.to_re ":") (re.range "0" "5") (re.range "0" "9"))))) +(assert (not (str.in_re X (re.++ (re.union (str.to_re "0") (re.++ (re.range "1" "9") ((_ re.loop 0 3) (re.range "0" "9"))) (re.++ (re.range "1" "5") ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (str.to_re "6") (re.range "0" "5") (re.range "0" "5") (re.union (re.++ (re.range "0" "2") (re.range "0" "9")) (re.++ (str.to_re "3") (re.range "0" "5"))))) (str.to_re "\u{a}"))))) +(assert (not (str.in_re X (re.++ (re.union (str.to_re "ac") (str.to_re "AC") (str.to_re "al") (str.to_re "AL") (str.to_re "am") (str.to_re "AM") (str.to_re "ap") (str.to_re "AP") (str.to_re "ba") (str.to_re "BA") (str.to_re "ce") (str.to_re "CE") (str.to_re "df") (str.to_re "DF") (str.to_re "es") (str.to_re "ES") (str.to_re "go") (str.to_re "GO") (str.to_re "ma") (str.to_re "MA") (str.to_re "mg") (str.to_re "MG") (str.to_re "ms") (str.to_re "MS") (str.to_re "mt") (str.to_re "MT") (str.to_re "pa") (str.to_re "PA") (str.to_re "pb") (str.to_re "PB") (str.to_re "pe") (str.to_re "PE") (str.to_re "pi") (str.to_re "PI") (str.to_re "pr") (str.to_re "PR") (str.to_re "rj") (str.to_re "RJ") (str.to_re "rn") (str.to_re "RN") (str.to_re "ro") (str.to_re "RO") (str.to_re "rr") (str.to_re "RR") (str.to_re "rs") (str.to_re "RS") (str.to_re "sc") (str.to_re "SC") (str.to_re "se") (str.to_re "SE") (str.to_re "sp") (str.to_re "SP") (str.to_re "to") (str.to_re "TO")) (str.to_re "\u{a}"))))) +(assert (not (str.in_re X (re.++ (re.union (re.++ (re.union (re.++ (re.* (str.to_re "0")) (re.range "1" "9")) (re.++ (re.union (str.to_re "1") (str.to_re "2")) (re.range "0" "9")) (re.++ (str.to_re "3") (re.union (str.to_re "0") (str.to_re "1")))) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (re.++ (re.* (str.to_re "0")) (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "8"))) (str.to_re "10") (str.to_re "12")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (re.++ (re.* (str.to_re "0")) (re.range "1" "9")) (re.++ (re.union (str.to_re "1") (str.to_re "2")) (re.range "0" "9")) (str.to_re "30")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (re.++ (re.* (str.to_re "0")) (re.union (str.to_re "4") (str.to_re "6") (str.to_re "9"))) (str.to_re "11")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (re.++ (re.* (str.to_re "0")) (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "8"))) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (str.to_re "02") (str.to_re "2")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (str.to_re "29") (re.union (str.to_re ".") (str.to_re "-") (str.to_re "/")) (re.union (str.to_re "02") (str.to_re "2")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (str.to_re "0") (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "0") (str.to_re "4") (str.to_re "8")) (str.to_re "00")) (re.++ (str.to_re "29") (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (str.to_re "02") (str.to_re "2")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "2") (str.to_re "6")) (str.to_re "00")) (re.++ (str.to_re "29") (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (str.to_re "02") (str.to_re "2")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.range "0" "9") (re.range "0" "9") (str.to_re "0") (re.union (str.to_re "4") (str.to_re "8"))) (re.++ (str.to_re "29") (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (str.to_re "02") (str.to_re "2")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.range "0" "9") (re.range "0" "9") (re.union (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "0") (str.to_re "4") (str.to_re "8"))) (re.++ (str.to_re "29") (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.union (str.to_re "02") (str.to_re "2")) (re.union (str.to_re "-") (str.to_re ".") (str.to_re "/")) (re.range "0" "9") (re.range "0" "9") (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "2") (str.to_re "6")))) (str.to_re "\u{a}"))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance08965.smt2 b/benchmarks/instance08965.smt2 new file mode 100644 index 000000000..4449c9d4e --- /dev/null +++ b/benchmarks/instance08965.smt2 @@ -0,0 +1,23 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (str.to_re "qr/") (re.union (str.to_re "Alabama") (str.to_re "Alaska") (str.to_re "Arizona") (str.to_re "Arkansas") (str.to_re "California") (str.to_re "Colorado") (str.to_re "Connecticut") (str.to_re "Delaware") (str.to_re "Florida") (str.to_re "Georgia") (str.to_re "Hawaii") (str.to_re "Idaho") (str.to_re "Illinois") (str.to_re "Indiana") (str.to_re "Iowa") (str.to_re "Kansas") (str.to_re "Kentucky") (str.to_re "Louisiana") (str.to_re "Maine") (str.to_re "Maryland") (str.to_re "Massachusetts") (str.to_re "Michigan") (str.to_re "Minnesota") (str.to_re "Mississippi") (str.to_re "Missouri") (str.to_re "Montana") (str.to_re "Nebraska") (str.to_re "Nevada") (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Hampshire")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Jersey")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Mexico")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "York")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Ohio") (str.to_re "Oklahoma") (str.to_re "Oregon") (str.to_re "Pennsylvania") (re.++ (str.to_re "Rhode") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Island")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Tennessee") (str.to_re "Texas") (str.to_re "Utah") (str.to_re "Vermont") (str.to_re "Virginia") (str.to_re "Washington") (re.++ (str.to_re "West") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Virginia")) (str.to_re "Wisconsin") (str.to_re "Wyoming")) (str.to_re "/\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "6") ((_ re.loop 7 7) (re.range "0" "9")) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "/Referer:") (re.+ (re.union (str.to_re "\u{d}") (str.to_re "\u{a}"))) (str.to_re "/.html\u{d}/Hsm\u{a}") ((_ re.loop 32 32) (re.union (str.to_re "_") (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (re.* (re.union (str.to_re "_") (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_")))))) +(assert (str.in_re X (re.++ (str.to_re "Wareztv.seekmo.com") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Keylogging\u{13}TRUSTYFILES.COM\u{a}")))) +(assert (not (str.in_re X (re.++ (str.to_re "Flooded") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Host:") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "AppName/GRSI|Server|\u{13}Host:origin=sidefindHost:User-Agent:\u{a}"))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance09159.smt2 b/benchmarks/instance09159.smt2 new file mode 100644 index 000000000..2d5e138d9 --- /dev/null +++ b/benchmarks/instance09159.smt2 @@ -0,0 +1,23 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status sat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (str.to_re "__") (re.+ re.allchar) (str.to_re "__\u{a}"))))) +(assert (not (str.in_re X (re.++ (str.to_re "/.avi") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}"))))) +(assert (not (str.in_re X (re.++ (str.to_re "User") (re.* re.allchar) (str.to_re "User-Agent:") (re.* re.allchar) (str.to_re "ResultATTENTION:riggiymd/wdhi.vhi\u{a}"))))) +(assert (str.in_re X (re.++ (re.union (re.++ (str.to_re "A") (re.union (str.to_re "BW") (str.to_re "FG") (str.to_re "GO") (str.to_re "IA") (re.++ (str.to_re "L") (re.union (str.to_re "A") (str.to_re "B"))) (re.++ (str.to_re "N") (re.union (str.to_re "D") (str.to_re "T"))) (re.++ (str.to_re "R") (re.union (str.to_re "E") (str.to_re "G") (str.to_re "M"))) (str.to_re "SM") (re.++ (str.to_re "T") (re.union (str.to_re "A") (str.to_re "F") (str.to_re "G"))) (re.++ (str.to_re "U") (re.union (str.to_re "S") (str.to_re "T"))) (str.to_re "ZE"))) (re.++ (str.to_re "B") (re.union (str.to_re "DI") (re.++ (str.to_re "E") (re.union (str.to_re "L") (str.to_re "N"))) (str.to_re "FA") (re.++ (str.to_re "G") (re.union (str.to_re "D") (str.to_re "R"))) (re.++ (str.to_re "H") (re.union (str.to_re "R") (str.to_re "S"))) (str.to_re "IH") (re.++ (str.to_re "L") (re.union (str.to_re "M") (str.to_re "R") (str.to_re "Z"))) (str.to_re "MU") (str.to_re "OL") (re.++ (str.to_re "R") (re.union (str.to_re "A") (str.to_re "B") (str.to_re "N"))) (str.to_re "TN") (str.to_re "VT") (str.to_re "WA"))) (re.++ (str.to_re "C") (re.union (re.++ (str.to_re "A") (re.union (str.to_re "F") (str.to_re "N"))) (str.to_re "CK") (re.++ (str.to_re "H") (re.union (str.to_re "E") (str.to_re "L") (str.to_re "N"))) (str.to_re "IV") (str.to_re "MR") (re.++ (str.to_re "O") (re.union (str.to_re "D") (str.to_re "G") (str.to_re "K") (str.to_re "L") (str.to_re "M"))) (str.to_re "PV") (str.to_re "RI") (str.to_re "UB") (str.to_re "XR") (re.++ (str.to_re "Y") (re.union (str.to_re "M") (str.to_re "P"))) (str.to_re "ZE"))) (re.++ (str.to_re "D") (re.union (str.to_re "EU") (str.to_re "JI") (str.to_re "MA") (str.to_re "NK") (str.to_re "OM") (str.to_re "ZA"))) (re.++ (str.to_re "E") (re.union (str.to_re "CU") (str.to_re "GY") (str.to_re "RI") (re.++ (str.to_re "S") (re.union (str.to_re "H") (str.to_re "P") (str.to_re "T"))) (str.to_re "TH"))) (re.++ (str.to_re "F") (re.union (str.to_re "IN") (str.to_re "JI") (str.to_re "LK") (re.++ (str.to_re "R") (re.union (str.to_re "A") (str.to_re "O"))) (str.to_re "SM"))) (re.++ (str.to_re "G") (re.union (str.to_re "AB") (str.to_re "BR") (str.to_re "EO") (str.to_re "GY") (str.to_re "HA") (re.++ (str.to_re "I") (re.union (str.to_re "B") (str.to_re "N"))) (str.to_re "LP") (str.to_re "MB") (str.to_re "NQ") (str.to_re "NB") (re.++ (str.to_re "R") (re.union (str.to_re "C") (str.to_re "D") (str.to_re "L"))) (str.to_re "TM") (re.++ (str.to_re "U") (re.union (str.to_re "F") (str.to_re "M") (str.to_re "Y"))))) (re.++ (str.to_re "H") (re.union (str.to_re "KG") (str.to_re "MD") (str.to_re "ND") (str.to_re "RV") (str.to_re "TI") (str.to_re "UN"))) (re.++ (str.to_re "I") (re.union (str.to_re "DN") (str.to_re "MN") (str.to_re "ND") (str.to_re "OT") (re.++ (str.to_re "R") (re.union (str.to_re "L") (str.to_re "N") (str.to_re "Q"))) (re.++ (str.to_re "S") (re.union (str.to_re "L") (str.to_re "R"))) (str.to_re "TA"))) (re.++ (str.to_re "J") (re.union (str.to_re "AM") (str.to_re "EY") (str.to_re "OR") (str.to_re "PN"))) (re.++ (str.to_re "K") (re.union (str.to_re "AZ") (str.to_re "EN") (str.to_re "GZ") (str.to_re "HM") (str.to_re "IR") (str.to_re "NA") (str.to_re "OR") (str.to_re "WT"))) (re.++ (str.to_re "L") (re.union (str.to_re "AO") (re.++ (str.to_re "B") (re.union (str.to_re "N") (str.to_re "R") (str.to_re "Y"))) (str.to_re "CA") (str.to_re "IE") (str.to_re "KA") (str.to_re "SO") (str.to_re "TU") (str.to_re "UX") (str.to_re "VA"))) (re.++ (str.to_re "M") (re.union (re.++ (str.to_re "A") (re.union (str.to_re "C") (str.to_re "F") (str.to_re "R"))) (str.to_re "CO") (re.++ (str.to_re "D") (re.union (str.to_re "A") (str.to_re "G") (str.to_re "V"))) (str.to_re "EX") (str.to_re "HL") (str.to_re "KD") (re.++ (str.to_re "L") (re.union (str.to_re "I") (str.to_re "T"))) (str.to_re "MR") (re.++ (str.to_re "N") (re.union (str.to_re "E") (str.to_re "G") (str.to_re "P"))) (str.to_re "OZ") (str.to_re "RT") (str.to_re "SR") (str.to_re "TQ") (str.to_re "US") (str.to_re "WI") (re.++ (str.to_re "Y") (re.union (str.to_re "S") (str.to_re "T"))))) (re.++ (str.to_re "N") (re.union (str.to_re "AM") (str.to_re "CL") (str.to_re "ER") (str.to_re "FK") (str.to_re "GA") (re.++ (str.to_re "I") (re.union (str.to_re "C") (str.to_re "U"))) (str.to_re "LD") (str.to_re "OR") (str.to_re "PL") (str.to_re "RU") (str.to_re "ZL"))) (str.to_re "OMN") (re.++ (str.to_re "P") (re.union (re.++ (str.to_re "A") (re.union (str.to_re "K") (str.to_re "N"))) (str.to_re "CN") (str.to_re "ER") (str.to_re "HL") (str.to_re "LW") (str.to_re "NG") (str.to_re "OL") (re.++ (str.to_re "R") (re.union (str.to_re "I") (str.to_re "K") (str.to_re "T") (str.to_re "Y"))) (str.to_re "SE") (str.to_re "YF"))) (str.to_re "QAT") (re.++ (str.to_re "R") (re.union (str.to_re "EU") (str.to_re "OU") (str.to_re "US") (str.to_re "WA"))) (re.++ (str.to_re "S") (re.union (str.to_re "AU") (str.to_re "DN") (str.to_re "EN") (re.++ (str.to_re "G") (re.union (str.to_re "P") (str.to_re "S"))) (str.to_re "HN") (str.to_re "JM") (re.++ (str.to_re "L") (re.union (str.to_re "B") (str.to_re "E") (str.to_re "V"))) (str.to_re "MR") (str.to_re "OM") (str.to_re "PM") (str.to_re "RB") (str.to_re "TP") (str.to_re "UR") (re.++ (str.to_re "V") (re.union (str.to_re "K") (str.to_re "N"))) (re.++ (str.to_re "W") (re.union (str.to_re "E") (str.to_re "Z"))) (re.++ (str.to_re "Y") (re.union (str.to_re "C") (str.to_re "R"))))) (re.++ (str.to_re "T") (re.union (re.++ (str.to_re "C") (re.union (str.to_re "A") (str.to_re "D"))) (str.to_re "GO") (str.to_re "HA") (str.to_re "JK") (re.++ (str.to_re "K") (re.union (str.to_re "L") (str.to_re "M"))) (str.to_re "LS") (str.to_re "ON") (str.to_re "TO") (re.++ (str.to_re "U") (re.union (str.to_re "N") (str.to_re "R") (str.to_re "V"))) (str.to_re "WN") (str.to_re "ZA"))) (re.++ (str.to_re "U") (re.union (str.to_re "EN") (str.to_re "GA") (str.to_re "KR") (str.to_re "MI") (str.to_re "RY") (str.to_re "SA") (str.to_re "ZB"))) (re.++ (str.to_re "V") (re.union (str.to_re "AT") (str.to_re "CT") (str.to_re "GB") (str.to_re "IR") (str.to_re "NM") (str.to_re "UT"))) (re.++ (str.to_re "W") (re.union (str.to_re "LF") (str.to_re "SM"))) (str.to_re "YEM") (re.++ (str.to_re "Z") (re.union (str.to_re "AF") (str.to_re "MB") (str.to_re "WE")))) (str.to_re "\u{a}")))) +(assert (not (str.in_re X (re.++ (re.* (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re "-") ((_ re.loop 2 2) (re.range "0" "9")))) (str.to_re "\u{a}"))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance11213.smt2 b/benchmarks/instance11213.smt2 new file mode 100644 index 000000000..0bdec4a17 --- /dev/null +++ b/benchmarks/instance11213.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (str.to_re "//") ((_ re.loop 48 48) (re.union (str.to_re "-") (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "/U\u{a}"))))) +(assert (str.in_re X (re.++ (re.opt (re.++ (re.opt (str.to_re " ")) (re.opt (str.to_re "+")) (str.to_re "34"))) (re.union (re.++ (str.to_re "6") (re.union ((_ re.loop 8 8) (re.range "0" "9")) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 6 6) (re.range "0" "9"))) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9"))))) (re.++ (str.to_re "9") (re.union ((_ re.loop 8 8) (re.range "0" "9")) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 6 6) (re.range "0" "9"))) (re.++ (re.range "1" "9") (str.to_re " ") ((_ re.loop 7 7) (re.range "0" "9"))) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 3 3) (re.range "0" "9"))) (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re " ") ((_ re.loop 2 2) (re.range "0" "9")))))) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.++ (re.+ (re.union (re.range "a" "z") (re.range "A" "Z") (re.range "0" "9") (str.to_re ".") (str.to_re "-") (str.to_re "_") (str.to_re "'") (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.union (re.++ (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general") (str.to_re "unicode") (str.to_re "roman") (str.to_re "slovak") (str.to_re "czech") (str.to_re "icelandic") (re.++ (re.union (str.to_re "latv") (str.to_re "pers")) (str.to_re "ian")) (re.++ (re.union (str.to_re "dan") (str.to_re "pol") (str.to_re "span") (str.to_re "swed") (str.to_re "turk")) (str.to_re "ish")) (str.to_re "spanish2") (re.++ (re.union (str.to_re "esto") (str.to_re "lithua") (str.to_re "roma") (str.to_re "slove")) (str.to_re "nian_ci"))) (str.to_re "u") (re.union (str.to_re "cs2") (str.to_re "tf8"))) (re.++ (re.union (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "1256"))) (str.to_re "armscii8") (str.to_re "geostd8") (str.to_re "ascii") (str.to_re "keybcs2") (str.to_re "greek") (str.to_re "hebrew") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general_ci"))) (re.++ (re.union (str.to_re "dec8") (str.to_re "swe7")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "swedish_ci"))) (re.++ (re.union (str.to_re "hp8") (str.to_re "latin5")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "english_ci"))) (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "gb") (re.union (str.to_re "2312") (str.to_re "k")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "chinese_ci"))) (re.++ (re.union (str.to_re "cp932") (str.to_re "eucjpms") (re.++ (re.union (str.to_re "s") (str.to_re "u")) (str.to_re "jis"))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "japanese_ci"))) (re.++ (str.to_re "euckr_") (re.union (str.to_re "bin") (str.to_re "korean_ci"))) (re.++ (str.to_re "tis620_") (re.union (str.to_re "bin") (str.to_re "thai_ci"))) (re.++ (str.to_re "latin1_") (re.union (str.to_re "bin") (re.++ (re.union (re.++ (re.union (str.to_re "dan") (str.to_re "span") (str.to_re "swed")) (str.to_re "ish")) (re.++ (str.to_re "german") (re.union (str.to_re "1") (str.to_re "2")))) (str.to_re "_ci")) (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))))) (re.++ (str.to_re "cp1250_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (str.to_re "general_ci"))) (re.++ (str.to_re "latin2_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (re.++ (re.union (str.to_re "general") (str.to_re "hungarian") (str.to_re "croatian")) (str.to_re "_ci")))) (re.++ (str.to_re "cp1257_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "lithuanian")) (str.to_re "_ci")))) (re.++ (str.to_re "latin7_") (re.union (str.to_re "bin") (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))) (str.to_re "estonian_cs"))) (re.++ (str.to_re "\u{a}cp1251_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "bulgarian") (str.to_re "ukrainian")) (str.to_re "_ci")) (str.to_re "general_cs")))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance11705.smt2 b/benchmarks/instance11705.smt2 new file mode 100644 index 000000000..2c344ae0e --- /dev/null +++ b/benchmarks/instance11705.smt2 @@ -0,0 +1,23 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (str.to_re "pjpoptwql/rlnj") (re.+ (re.range "0" "9")) (str.to_re "waiting") (re.+ (re.range "0" "9")) (str.to_re "ocllceclbhs/gth") (re.+ (re.union (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "gdvsotuqwsg/dxt.hdUser-Agent:\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "Host:") (re.range "0" "9") (str.to_re "Keylogger") (re.* re.allchar) (str.to_re "Onetrustyfiles.com\u{a}")))) +(assert (str.in_re X (re.++ ((_ re.loop 2 2) (re.range "0" "9")) (str.to_re "-") (re.union (str.to_re "Jan") (str.to_re "Feb") (str.to_re "Mar") (str.to_re "Apr") (str.to_re "May") (str.to_re "Jun") (str.to_re "Jul") (str.to_re "Aug") (str.to_re "Sep") (str.to_re "Oct") (str.to_re "Nov") (str.to_re "Dec") (str.to_re "jan") (str.to_re "feb") (str.to_re "mar") (str.to_re "apr") (str.to_re "may") (str.to_re "jun") (str.to_re "jul") (str.to_re "aug") (str.to_re "sep") (str.to_re "oct") (str.to_re "nov") (str.to_re "dec") (str.to_re "JAN") (str.to_re "FEB") (str.to_re "MAR") (str.to_re "APR") (str.to_re "MAY") (str.to_re "JUN") (str.to_re "JUL") (str.to_re "AUG") (str.to_re "SEP") (str.to_re "OCT") (str.to_re "NOV") (str.to_re "DEC")) (str.to_re "-") ((_ re.loop 4 4) (re.range "0" "9")) (str.to_re "\u{a}")))) +(assert (not (str.in_re X (re.++ (re.range "\u{80}" "\u{ff}") (str.to_re "\u{a}"))))) +(assert (str.in_re X (re.++ (str.to_re "/.xlw") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance11745.smt2 b/benchmarks/instance11745.smt2 new file mode 100644 index 000000000..246a3f777 --- /dev/null +++ b/benchmarks/instance11745.smt2 @@ -0,0 +1,21 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.union (str.to_re "EMA") (str.to_re "QCY") (str.to_re "SQZ") (str.to_re "ORM") (str.to_re "NQT") (str.to_re "WTN") (str.to_re "CBG") (str.to_re "QFO") (str.to_re "BEQ") (str.to_re "LKZ") (str.to_re "LTN") (str.to_re "KNF") (str.to_re "MHZ") (str.to_re "NWI") (str.to_re "CLF") (str.to_re "QUY") (str.to_re "SEN") (str.to_re "STN") (str.to_re "BEQ") (str.to_re "BQH") (str.to_re "LHR") (str.to_re "NHT") (str.to_re "LCY") (str.to_re "MME") (str.to_re "NCL") (str.to_re "BWF") (str.to_re "BLK") (str.to_re "CAX") (str.to_re "LPL") (str.to_re "MAN") (str.to_re "BBP") (str.to_re "BEX") (str.to_re "BZZ") (str.to_re "LGW") (str.to_re "SOU") (str.to_re "FAB") (str.to_re "OXF") (str.to_re "ESH") (str.to_re "QLA") (str.to_re "LYX") (str.to_re "KRH") (str.to_re "ODH") (str.to_re "RCS") (str.to_re "QUC") (str.to_re "BBS") (str.to_re "GLO") (str.to_re "EXT") (str.to_re "FFD") (str.to_re "BOH") (str.to_re "LYE") (str.to_re "NQY") (str.to_re "LEQ") (str.to_re "ISC") (str.to_re "UPV") (str.to_re "BRS") (str.to_re "YEO") (str.to_re "CVT") (str.to_re "BHX") (str.to_re "DSA") (str.to_re "HUY") (str.to_re "LBA") (str.to_re "HRT") (str.to_re "BFS") (str.to_re "BHD") (str.to_re "LDY") (str.to_re "ENK") (str.to_re "ABZ") (str.to_re "OBN") (str.to_re "BEB") (str.to_re "BRR") (str.to_re "CAL") (str.to_re "COL") (str.to_re "CSA") (str.to_re "NRL") (str.to_re "INV") (str.to_re "SCS") (str.to_re "DND") (str.to_re "LSI") (str.to_re "EOI") (str.to_re "EDI") (str.to_re "FIE") (str.to_re "FOA") (str.to_re "ILY") (str.to_re "FSS") (str.to_re "NDY") (str.to_re "ADX") (str.to_re "LMO") (str.to_re "OUK") (str.to_re "PSV") (str.to_re "PPW") (str.to_re "PIK") (str.to_re "GLA") (str.to_re "KOI") (str.to_re "PSL") (str.to_re "SYY") (str.to_re "SKL") (str.to_re "SOY") (str.to_re "LWK") (str.to_re "TRE") (str.to_re "WRY") (str.to_re "WHS") (str.to_re "WIC") (str.to_re "HAW") (str.to_re "CEG") (str.to_re "VLY") (str.to_re "SWS") (str.to_re "CWL") (str.to_re "DGX") (str.to_re "ACI") (str.to_re "GCI") (str.to_re "IOM") (str.to_re "JER\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "/User-Agent: ") ((_ re.loop 9 9) (re.range "A" "Z")) (str.to_re "\u{d}\u{a}/Hm\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "Admin") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "daosearch.comMyPostwww.raxsearch.comref=%user_id\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance11856.smt2 b/benchmarks/instance11856.smt2 new file mode 100644 index 000000000..0c9a4d020 --- /dev/null +++ b/benchmarks/instance11856.smt2 @@ -0,0 +1,21 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status sat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (str.to_re "/filename=") (re.* (re.comp (str.to_re "\u{a}"))) (str.to_re ".addin/i\u{a}"))))) +(assert (not (str.in_re X (re.++ (str.to_re "//") ((_ re.loop 5 5) (re.range "0" "9")) (str.to_re ".jar/U\u{a}"))))) +(assert (str.in_re X (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "euc") (re.union (str.to_re "kr") (str.to_re "jpms"))) (str.to_re "binary") (str.to_re "greek") (str.to_re "tis620") (str.to_re "hebrew") (str.to_re "ascii") (str.to_re "swe7") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u"))) (re.++ (re.union (str.to_re "u") (str.to_re "keyb")) (str.to_re "cs2")) (re.++ (re.union (str.to_re "dec") (str.to_re "hp") (str.to_re "utf") (str.to_re "geostd") (str.to_re "armscii")) (str.to_re "8")) (re.++ (str.to_re "gb") (re.union (str.to_re "k") (str.to_re "2312"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "932") (re.++ (str.to_re "125") (re.union (str.to_re "0") (str.to_re "1") (str.to_re "6") (str.to_re "7"))))) (re.++ (str.to_re "latin") (re.union (str.to_re "1") (str.to_re "2") (str.to_re "5") (str.to_re "7"))) (re.++ (re.union (str.to_re "u") (str.to_re "s")) (str.to_re "jis")) (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman")))) (str.to_re "\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance12204.smt2 b/benchmarks/instance12204.smt2 new file mode 100644 index 000000000..4a192538c --- /dev/null +++ b/benchmarks/instance12204.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (re.* (re.range "0" "9")) (re.+ (re.range "1" "9")) (re.* (re.range "0" "9")) (str.to_re "\u{a}"))))) +(assert (not (str.in_re X (re.++ (str.to_re "/.svg") (re.opt (str.to_re "z")) (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}"))))) +(assert (str.in_re X (re.++ (str.to_re "<") (re.opt (str.to_re "/")) (re.union (str.to_re "a") (str.to_re "abbr") (str.to_re "acronym") (str.to_re "address") (str.to_re "applet") (str.to_re "area") (str.to_re "b") (str.to_re "base") (str.to_re "basefont") (str.to_re "bdo") (str.to_re "big") (str.to_re "blockquote") (str.to_re "body") (str.to_re "br") (str.to_re "button") (str.to_re "caption") (str.to_re "center") (str.to_re "cite") (str.to_re "code") (str.to_re "col") (str.to_re "colgroup") (str.to_re "dd") (str.to_re "del") (str.to_re "dir") (str.to_re "div") (str.to_re "dfn") (str.to_re "dl") (str.to_re "dt") (str.to_re "em") (str.to_re "fieldset") (str.to_re "font") (str.to_re "form") (str.to_re "frame") (str.to_re "frameset") (re.++ (str.to_re "h") (re.range "1" "6")) (str.to_re "head") (str.to_re "hr") (str.to_re "html") (str.to_re "i") (str.to_re "iframe") (str.to_re "img") (str.to_re "input") (str.to_re "ins") (str.to_re "isindex") (str.to_re "kbd") (str.to_re "label") (str.to_re "legend") (str.to_re "li") (str.to_re "link") (str.to_re "map") (str.to_re "menu") (str.to_re "meta") (str.to_re "noframes") (str.to_re "noscript") (str.to_re "object") (str.to_re "ol") (str.to_re "optgroup") (str.to_re "option") (str.to_re "p") (str.to_re "param") (str.to_re "pre") (str.to_re "q") (str.to_re "s") (str.to_re "samp") (str.to_re "script") (str.to_re "select") (str.to_re "small") (str.to_re "span") (str.to_re "strike") (str.to_re "strong") (str.to_re "style") (str.to_re "sub") (str.to_re "sup") (str.to_re "table") (str.to_re "tbody") (str.to_re "td") (str.to_re "textarea") (str.to_re "tfoot") (str.to_re "th") (str.to_re "thead") (str.to_re "title") (str.to_re "tr") (str.to_re "tt") (str.to_re "u") (str.to_re "ul") (str.to_re "var") (str.to_re "xmp")) (re.* (re.union (re.* (re.union (re.++ (str.to_re "\u{22}") (re.* (re.comp (str.to_re "\u{22}"))) (str.to_re "\u{22}")) (re.++ (str.to_re "'") (re.* (re.comp (str.to_re "'"))) (str.to_re "'")))) (str.to_re "\u{22}") (str.to_re "'") (str.to_re ">"))) (str.to_re ">\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "/SOAPAction:") (re.* (re.union (str.to_re "\u{d}") (str.to_re "\u{a}"))) (str.to_re "Get") (re.union (str.to_re "ServerTime") (str.to_re "FileList") (str.to_re "File")) (str.to_re "\u{22}/i\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance12488.smt2 b/benchmarks/instance12488.smt2 new file mode 100644 index 000000000..b62061cb5 --- /dev/null +++ b/benchmarks/instance12488.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (re.range "1" "9") (re.range "0" "9") (re.range "0" "9") (re.range "0" "9") (re.range "0" "9") (re.range "0" "9") (str.to_re "\u{a}"))))) +(assert (str.in_re X (re.++ (str.to_re "/.s3m") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) +(assert (str.in_re X (re.++ ((_ re.loop 7 8) (re.range "0" "9")) (str.to_re "\u{a}0") (re.union (str.to_re "2") (str.to_re "|") (str.to_re "3") (str.to_re "4") (str.to_re "5") (str.to_re "6") (str.to_re "8") (str.to_re "9") (str.to_re "7"))))) +(assert (str.in_re X (re.++ (re.+ (re.union (str.to_re "_") (re.range "a" "z") (re.range "0" "9") (str.to_re "-"))) (re.* (re.++ (str.to_re ".") (re.+ (re.union (str.to_re "_") (re.range "a" "z") (re.range "0" "9") (str.to_re "-"))))) (str.to_re "@") (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))) (re.opt (re.++ (re.opt (str.to_re "-")) (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))))) (re.* (re.++ (str.to_re ".") (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))) (re.opt (re.++ (re.opt (str.to_re "-")) (re.+ (re.union (re.range "a" "z") (re.range "0" "9"))))))) (str.to_re ".") (re.union ((_ re.loop 2 2) (re.range "a" "z")) (re.++ (str.to_re "xn") ((_ re.loop 2 2) (str.to_re "-")) ((_ re.loop 4 18) (re.union (re.range "a" "z") (re.range "0" "9")))) (str.to_re "arpa") (str.to_re "aero") (str.to_re "asia") (str.to_re "biz") (str.to_re "cat") (str.to_re "com") (str.to_re "coop") (str.to_re "edu") (str.to_re "gov") (str.to_re "info") (str.to_re "int") (str.to_re "jobs") (str.to_re "mil") (str.to_re "mobi") (str.to_re "museum") (str.to_re "name") (str.to_re "net") (str.to_re "org") (str.to_re "pro") (str.to_re "tel") (str.to_re "travel") (str.to_re "xxx")) (str.to_re "\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance12671.smt2 b/benchmarks/instance12671.smt2 new file mode 100644 index 000000000..164fbb7ed --- /dev/null +++ b/benchmarks/instance12671.smt2 @@ -0,0 +1,21 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.union (re.++ (re.union (re.++ (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (str.to_re "30")) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "P") (str.to_re ",") (str.to_re "p")) (re.union (str.to_re "R") (str.to_re ",") (str.to_re "r"))) (re.++ (re.union (str.to_re "J") (str.to_re ",") (str.to_re "j")) (re.union (str.to_re "U") (str.to_re ",") (str.to_re "u")) (re.union (str.to_re "N") (str.to_re ",") (str.to_re "n"))) (re.++ (re.union (str.to_re "S") (str.to_re ",") (str.to_re "s")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "P") (str.to_re ",") (str.to_re "p"))) (re.++ (re.union (str.to_re "N") (str.to_re ",") (str.to_re "n")) (re.union (str.to_re "O") (str.to_re ",") (str.to_re "o")) (re.union (str.to_re "V") (str.to_re ",") (str.to_re "v"))))) (re.++ (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (re.++ (str.to_re "3") (re.range "0" "1"))) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "J") (str.to_re ",") (str.to_re "j")) (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "N") (str.to_re ",") (str.to_re "n"))) (re.++ (re.union (str.to_re "M") (str.to_re ",") (str.to_re "m")) (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "R") (str.to_re ",") (str.to_re "r"))) (re.++ (re.union (str.to_re "M") (str.to_re ",") (str.to_re "m")) (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "Y") (str.to_re ",") (str.to_re "y"))) (re.++ (re.union (str.to_re "J") (str.to_re ",") (str.to_re "j")) (re.union (str.to_re "U") (str.to_re ",") (str.to_re "u")) (re.union (str.to_re "L") (str.to_re ",") (str.to_re "l"))) (re.++ (re.union (str.to_re "A") (str.to_re ",") (str.to_re "a")) (re.union (str.to_re "U") (str.to_re ",") (str.to_re "u")) (re.union (str.to_re "G") (str.to_re ",") (str.to_re "g"))) (re.++ (re.union (str.to_re "O") (str.to_re ",") (str.to_re "o")) (re.union (str.to_re "C") (str.to_re ",") (str.to_re "c")) (re.union (str.to_re "T") (str.to_re ",") (str.to_re "t"))) (re.++ (re.union (str.to_re "D") (str.to_re ",") (str.to_re "d")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "C") (str.to_re ",") (str.to_re "c")))))) (str.to_re "-") ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "8"))) (str.to_re "--") ((_ re.loop 2 2) (re.range "0" "9")) (re.union (re.++ (re.union (str.to_re "0") (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "1") (str.to_re "2") (str.to_re "3") (str.to_re "5") (str.to_re "6") (str.to_re "7") (str.to_re "9"))) (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "0") (str.to_re "1") (str.to_re "3") (str.to_re "4") (str.to_re "5") (str.to_re "7") (str.to_re "8") (str.to_re "9")))) (re.union (str.to_re "F") (str.to_re ",") (str.to_re "f")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "B") (str.to_re ",") (str.to_re "b"))) (re.++ (str.to_re "\u{a}") (re.union (re.range "1" "9") (re.++ (str.to_re "0") (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "9"))) (str.to_re "--") ((_ re.loop 2 2) (re.range "0" "9")) (re.union (re.++ (re.union (str.to_re "0") (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "0") (str.to_re "4") (str.to_re "8"))) (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "2") (str.to_re "6")))) (re.union (str.to_re "F") (str.to_re ",") (str.to_re "f")) (re.union (str.to_re "E") (str.to_re ",") (str.to_re "e")) (re.union (str.to_re "B") (str.to_re ",") (str.to_re "b")))))) +(assert (str.in_re X (re.union (re.++ (re.union (re.range "0" "9") (re.++ (re.range "0" "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "3"))) (str.to_re ":") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (re.union (str.to_re "AM") (str.to_re "PM") (str.to_re "am") (str.to_re "pm") (str.to_re "aM") (str.to_re "Am") (str.to_re "pM") (re.++ (str.to_re "P") ((_ re.loop 2 2) (str.to_re "m")))) (re.range "0" "5") (re.range "0" "9")) (re.++ (str.to_re "\u{a}") (re.union (re.range "0" "9") (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "3"))) (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (re.union (str.to_re "AM") (str.to_re "PM") (str.to_re "am") (str.to_re "pm") (str.to_re "aM") (str.to_re "Am") (str.to_re "pM") (re.++ (str.to_re "P") ((_ re.loop 2 2) (str.to_re "m")))))))) +(assert (str.in_re X (re.++ (str.to_re "Points") (re.+ (re.range "0" "9")) (str.to_re "Host:") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "toBasicwww.webcruiser.cc\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance12768.smt2 b/benchmarks/instance12768.smt2 new file mode 100644 index 000000000..361639b63 --- /dev/null +++ b/benchmarks/instance12768.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (str.to_re "/User-Agent:") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Ryeol") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "HTTP") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Client") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "Class/smiH\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "Spyware") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "ToolBar") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "User-Agent:MM_RECO.EXEToClientonAlert\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "ver") (re.+ (re.range "0" "9")) (str.to_re "sports") (re.+ (re.union (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "whenu.com\u{13}wp-includes/feed.php?\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "qr/") (re.union (str.to_re "Alabama") (str.to_re "Alaska") (str.to_re "Arizona") (str.to_re "Arkansas") (str.to_re "California") (str.to_re "Colorado") (str.to_re "Connecticut") (str.to_re "Delaware") (str.to_re "Florida") (str.to_re "Georgia") (str.to_re "Hawaii") (str.to_re "Idaho") (str.to_re "Illinois") (str.to_re "Indiana") (str.to_re "Iowa") (str.to_re "Kansas") (str.to_re "Kentucky") (str.to_re "Louisiana") (str.to_re "Maine") (str.to_re "Maryland") (str.to_re "Massachusetts") (str.to_re "Michigan") (str.to_re "Minnesota") (str.to_re "Mississippi") (str.to_re "Missouri") (str.to_re "Montana") (str.to_re "Nebraska") (str.to_re "Nevada") (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Hampshire")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Jersey")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Mexico")) (re.++ (str.to_re "New") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "York")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "North") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Ohio") (str.to_re "Oklahoma") (str.to_re "Oregon") (str.to_re "Pennsylvania") (re.++ (str.to_re "Rhode") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Island")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Carolina")) (re.++ (str.to_re "South") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Dakota")) (str.to_re "Tennessee") (str.to_re "Texas") (str.to_re "Utah") (str.to_re "Vermont") (str.to_re "Virginia") (str.to_re "Washington") (re.++ (str.to_re "West") (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "Virginia")) (str.to_re "Wisconsin") (str.to_re "Wyoming")) (str.to_re "/\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance12833.smt2 b/benchmarks/instance12833.smt2 new file mode 100644 index 000000000..1cbbd4099 --- /dev/null +++ b/benchmarks/instance12833.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (str.to_re "|Connected") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "adblock.linkz.com\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "//u\u{a}") (re.range "\u{0}" "\u{ff}") (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))))) +(assert (str.in_re X (re.++ (re.* (re.++ (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.union (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7"))) (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8"))) (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8"))) (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.* (re.++ (re.union (str.to_re "2") (str.to_re "5") (str.to_re "8")) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7")))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))) (re.union (str.to_re "1") (str.to_re "4") (str.to_re "7"))))) (re.* (re.union (str.to_re "0") (str.to_re "3") (str.to_re "6") (str.to_re "9"))))) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "/.pui") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance13062.smt2 b/benchmarks/instance13062.smt2 new file mode 100644 index 000000000..06bb16d4e --- /dev/null +++ b/benchmarks/instance13062.smt2 @@ -0,0 +1,23 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (str.to_re "/filename") (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "=") (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (re.* (re.union (str.to_re "\u{d}") (str.to_re "\u{a}"))) (str.to_re ".swf") (re.union (str.to_re "\u{22}") (str.to_re "'") (str.to_re ";") (str.to_re "\u{d}") (str.to_re "\u{a}") (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "/i\u{a}"))))) +(assert (not (str.in_re X (re.++ (re.union (re.++ (str.to_re "A") (re.union (str.to_re "L") (str.to_re "K") (str.to_re "S") (str.to_re "Z") (str.to_re "R") (str.to_re "A") (str.to_re "E") (str.to_re "P"))) (re.++ (str.to_re "C") (re.union (str.to_re "A") (str.to_re "O") (str.to_re "T"))) (re.++ (str.to_re "D") (re.union (str.to_re "E") (str.to_re "C"))) (re.++ (str.to_re "F") (re.union (str.to_re "L") (str.to_re "M"))) (re.++ (str.to_re "G") (re.union (str.to_re "A") (str.to_re "U"))) (str.to_re "HI") (re.++ (str.to_re "I") (re.union (str.to_re "A") (str.to_re "D") (str.to_re "L") (str.to_re "N"))) (re.++ (str.to_re "K") (re.union (str.to_re "S") (str.to_re "Y"))) (str.to_re "LA") (re.++ (str.to_re "M") (re.union (str.to_re "A") (str.to_re "D") (str.to_re "E") (str.to_re "H") (str.to_re "I") (str.to_re "N") (str.to_re "O") (str.to_re "P") (str.to_re "S") (str.to_re "T"))) (re.++ (str.to_re "N") (re.union (str.to_re "C") (str.to_re "D") (str.to_re "E") (str.to_re "H") (str.to_re "J") (str.to_re "M") (str.to_re "V") (str.to_re "Y"))) (re.++ (str.to_re "O") (re.union (str.to_re "H") (str.to_re "K") (str.to_re "R"))) (re.++ (str.to_re "P") (re.union (str.to_re "A") (str.to_re "R") (str.to_re "W"))) (str.to_re "RI") (re.++ (str.to_re "S") (re.union (str.to_re "C") (str.to_re "D"))) (re.++ (str.to_re "T") (re.union (str.to_re "N") (str.to_re "X"))) (str.to_re "UT") (re.++ (str.to_re "V") (re.union (str.to_re "A") (str.to_re "I") (str.to_re "T"))) (re.++ (str.to_re "W") (re.union (str.to_re "A") (str.to_re "I") (str.to_re "V") (str.to_re "Y")))) (str.to_re "\u{a}"))))) +(assert (str.in_re X (re.++ (str.to_re "/.wmv") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}")))) +(assert (not (str.in_re X (re.++ (str.to_re "User-Agent:") (re.* re.allchar) (str.to_re "Host:") (re.* re.allchar) (str.to_re "w3whowww.sogou.com\u{a}"))))) +(assert (str.in_re X (re.++ (str.to_re "Guarded") (re.+ (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "ready") (re.+ (re.union (re.range "0" "9") (re.range "A" "Z") (re.range "a" "z") (str.to_re "_"))) (str.to_re "PARSERHost:A-311ServerUser-Agent:scn.mystoretoolbar.com\u{13}\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance13106.smt2 b/benchmarks/instance13106.smt2 new file mode 100644 index 000000000..f0a3462e3 --- /dev/null +++ b/benchmarks/instance13106.smt2 @@ -0,0 +1,23 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (str.to_re "security") (re.+ (re.range "0" "9")) (str.to_re "Redirector\u{22}ServerHost:X-Mailer:\u{13}\u{a}")))) +(assert (str.in_re X (re.++ (re.opt (re.++ (str.to_re "1") (re.union (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "-") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re ".") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "/") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.opt (re.++ (re.opt (str.to_re "(")) ((_ re.loop 1 1) (re.range "2" "9")) ((_ re.loop 2 2) (re.range "0" "9")) (re.opt (str.to_re ")")) (re.opt (re.union (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "-") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re ".") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "/") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))))) ((_ re.loop 3 3) (re.range "0" "9")) (re.opt (re.union (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "-") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re ".") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (re.++ (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) (str.to_re "/") (re.opt (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")))) (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) ((_ re.loop 4 4) (re.range "0" "9")) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.++ (str.to_re "/filename=") (re.* (re.comp (str.to_re "\u{a}"))) (str.to_re ".svg/i\u{a}")))) +(assert (not (str.in_re X (str.to_re "MyHost:toHost:WinSessionwww.urlblaze.netResultHost:\u{a}")))) +(assert (not (str.in_re X (re.++ (str.to_re "/filename=") (re.opt (re.union (str.to_re "\u{22}") (str.to_re "'"))) (re.* (re.comp (str.to_re "\u{a}"))) (str.to_re ".pif") (re.union (str.to_re "\u{22}") (str.to_re "'") (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (str.to_re "/si\u{a}"))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance13975.smt2 b/benchmarks/instance13975.smt2 new file mode 100644 index 000000000..af0baede7 --- /dev/null +++ b/benchmarks/instance13975.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (re.opt (str.to_re "D")) (re.opt (re.union (str.to_re "-") (str.to_re "D"))) ((_ re.loop 5 5) (re.range "0" "9")) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.union (re.++ (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general") (str.to_re "unicode") (str.to_re "roman") (str.to_re "slovak") (str.to_re "czech") (str.to_re "icelandic") (re.++ (re.union (str.to_re "latv") (str.to_re "pers")) (str.to_re "ian")) (re.++ (re.union (str.to_re "dan") (str.to_re "pol") (str.to_re "span") (str.to_re "swed") (str.to_re "turk")) (str.to_re "ish")) (str.to_re "spanish2") (re.++ (re.union (str.to_re "esto") (str.to_re "lithua") (str.to_re "roma") (str.to_re "slove")) (str.to_re "nian_ci"))) (str.to_re "u") (re.union (str.to_re "cs2") (str.to_re "tf8"))) (re.++ (re.union (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "1256"))) (str.to_re "armscii8") (str.to_re "geostd8") (str.to_re "ascii") (str.to_re "keybcs2") (str.to_re "greek") (str.to_re "hebrew") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "general_ci"))) (re.++ (re.union (str.to_re "dec8") (str.to_re "swe7")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "swedish_ci"))) (re.++ (re.union (str.to_re "hp8") (str.to_re "latin5")) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "english_ci"))) (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "gb") (re.union (str.to_re "2312") (str.to_re "k")))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "chinese_ci"))) (re.++ (re.union (str.to_re "cp932") (str.to_re "eucjpms") (re.++ (re.union (str.to_re "s") (str.to_re "u")) (str.to_re "jis"))) (str.to_re "_") (re.union (str.to_re "bin") (str.to_re "japanese_ci"))) (re.++ (str.to_re "euckr_") (re.union (str.to_re "bin") (str.to_re "korean_ci"))) (re.++ (str.to_re "tis620_") (re.union (str.to_re "bin") (str.to_re "thai_ci"))) (re.++ (str.to_re "latin1_") (re.union (str.to_re "bin") (re.++ (re.union (re.++ (re.union (str.to_re "dan") (str.to_re "span") (str.to_re "swed")) (str.to_re "ish")) (re.++ (str.to_re "german") (re.union (str.to_re "1") (str.to_re "2")))) (str.to_re "_ci")) (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))))) (re.++ (str.to_re "cp1250_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (str.to_re "general_ci"))) (re.++ (str.to_re "latin2_") (re.union (str.to_re "bin") (str.to_re "czech_cs") (re.++ (re.union (str.to_re "general") (str.to_re "hungarian") (str.to_re "croatian")) (str.to_re "_ci")))) (re.++ (str.to_re "cp1257_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "lithuanian")) (str.to_re "_ci")))) (re.++ (str.to_re "latin7_") (re.union (str.to_re "bin") (re.++ (str.to_re "general_c") (re.union (str.to_re "i") (str.to_re "s"))) (str.to_re "estonian_cs"))) (re.++ (str.to_re "\u{a}cp1251_") (re.union (str.to_re "bin") (re.++ (re.union (str.to_re "general") (str.to_re "bulgarian") (str.to_re "ukrainian")) (str.to_re "_ci")) (str.to_re "general_cs")))))) +(assert (not (str.in_re X (re.++ (str.to_re "/.cgm") (re.union (str.to_re "?") (str.to_re "\u{5c}") (str.to_re "/")) (str.to_re "/smiU\u{a}"))))) +(assert (str.in_re X (re.++ (re.union (str.to_re "\u{5c}") (str.to_re "s") (str.to_re "+") (str.to_re ",")) (str.to_re "\u{a}")))) +(check-sat) + +(exit) diff --git a/benchmarks/instance14260.smt2 b/benchmarks/instance14260.smt2 new file mode 100644 index 000000000..bf36054fc --- /dev/null +++ b/benchmarks/instance14260.smt2 @@ -0,0 +1,23 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (not (str.in_re X (re.++ (str.to_re "")) (re.* re.allchar) (str.to_re "\u{a}"))))) +(assert (str.in_re X (re.++ (re.union (re.++ (re.range "0" "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "3"))) (str.to_re ":\u{a}") (re.range "0" "5") (re.range "0" "9")))) +(assert (str.in_re X (re.++ (str.to_re "Password=\u{22}") (re.union (re.++ (str.to_re "{") (re.+ re.allchar) (str.to_re "}") (re.+ (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z"))) (re.* (str.to_re "="))) (re.+ (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z")))) (str.to_re "\u{22}\u{a}")))) +(assert (str.in_re X (re.++ (re.union (re.++ (re.union (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (re.++ (str.to_re "3") (re.range "0" "1"))) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "y") (str.to_re "Y"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "l") (str.to_re "L"))) (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "g") (str.to_re "G"))) (re.++ (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "c") (str.to_re "C")) (re.union (str.to_re "t") (str.to_re "T"))) (re.++ (re.union (str.to_re "d") (str.to_re "D")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "c") (str.to_re "C"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (str.to_re "30")) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "p") (str.to_re "P")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "s") (str.to_re "S")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "p") (str.to_re "P"))) (re.++ (re.union (str.to_re "n") (str.to_re "N")) (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "v") (str.to_re "V"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "8"))) (str.to_re "-") (re.union (str.to_re "f") (str.to_re "F")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "b") (str.to_re "B")))) (str.to_re "-20") (re.union (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "0") (str.to_re "1") (str.to_re "3") (str.to_re "4") (str.to_re "5") (str.to_re "7") (str.to_re "8") (str.to_re "9"))) (re.++ (re.union (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "1") (str.to_re "2") (str.to_re "3") (str.to_re "5") (str.to_re "6") (str.to_re "7") (str.to_re "9"))))) (re.++ (re.union (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (re.++ (str.to_re "3") (re.range "0" "1"))) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "m") (str.to_re "M")) (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "y") (str.to_re "Y"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "l") (str.to_re "L"))) (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "g") (str.to_re "G"))) (re.++ (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "c") (str.to_re "C")) (re.union (str.to_re "t") (str.to_re "T"))) (re.++ (re.union (str.to_re "d") (str.to_re "D")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "c") (str.to_re "C"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (re.range "1" "2") (re.range "0" "9")) (str.to_re "30")) (str.to_re "-") (re.union (re.++ (re.union (str.to_re "a") (str.to_re "A")) (re.union (str.to_re "p") (str.to_re "P")) (re.union (str.to_re "r") (str.to_re "R"))) (re.++ (re.union (str.to_re "j") (str.to_re "J")) (re.union (str.to_re "u") (str.to_re "U")) (re.union (str.to_re "n") (str.to_re "N"))) (re.++ (re.union (str.to_re "s") (str.to_re "S")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "p") (str.to_re "P"))) (re.++ (re.union (str.to_re "n") (str.to_re "N")) (re.union (str.to_re "o") (str.to_re "O")) (re.union (str.to_re "v") (str.to_re "V"))))) (re.++ (re.union (re.++ (re.opt (str.to_re "0")) (re.range "1" "9")) (re.++ (str.to_re "1") (re.range "0" "9")) (re.++ (str.to_re "2") (re.range "0" "9"))) (str.to_re "-") (re.union (str.to_re "f") (str.to_re "F")) (re.union (str.to_re "e") (str.to_re "E")) (re.union (str.to_re "b") (str.to_re "B")))) (str.to_re "-20") (re.union (re.++ (re.union (str.to_re "1") (str.to_re "3") (str.to_re "5") (str.to_re "7") (str.to_re "9")) (re.union (str.to_re "2") (str.to_re "6"))) (re.++ (re.union (str.to_re "2") (str.to_re "4") (str.to_re "6") (str.to_re "8")) (re.union (str.to_re "0") (str.to_re "4") (str.to_re "8")))))) (str.to_re "\u{a}")))) +(assert (not (str.in_re X (re.union (str.to_re "100") ((_ re.loop 1 2) (re.range "0" "9")) (re.++ ((_ re.loop 1 2) (re.range "0" "9")) (str.to_re ",") ((_ re.loop 1 3) (re.range "0" "9")) (str.to_re "\u{a}")))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance14326.smt2 b/benchmarks/instance14326.smt2 new file mode 100644 index 000000000..35b8ab5c2 --- /dev/null +++ b/benchmarks/instance14326.smt2 @@ -0,0 +1,21 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status sat) + +(declare-const X String) +(assert (not (str.in_re X (re.union (re.++ (re.union (str.to_re "Jan") (str.to_re "Feb") (str.to_re "Mar") (str.to_re "Apr") (str.to_re "May") (str.to_re "Jun") (str.to_re "Jul") (str.to_re "Aug") (str.to_re "Sep") (str.to_re "Oct") (str.to_re "Nov") (str.to_re "Dec")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) (re.* (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}"))) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (str.to_re "jan") (str.to_re "feb") (str.to_re "mar") (str.to_re "apr") (str.to_re "may") (str.to_re "jun") (str.to_re "jul") (str.to_re "aug") (str.to_re "sep") (str.to_re "oct") (str.to_re "nov") (str.to_re "dec")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (str.to_re "January") (str.to_re "February") (str.to_re "March") (str.to_re "April") (str.to_re "May") (str.to_re "June") (str.to_re "July") (str.to_re "August") (str.to_re "September") (str.to_re "October") (str.to_re "November") (str.to_re "December")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) ((_ re.loop 4 4) (re.range "0" "9"))) (re.++ (re.union (str.to_re "january") (str.to_re "february") (str.to_re "march") (str.to_re "april") (str.to_re "may") (str.to_re "june") (str.to_re "july") (str.to_re "august") (str.to_re "september") (str.to_re "october") (str.to_re "november") (str.to_re "december")) (re.* (str.to_re ",")) (re.union (str.to_re " ") (str.to_re "\u{9}") (str.to_re "\u{a}") (str.to_re "\u{c}") (str.to_re "\u{d}")) ((_ re.loop 4 4) (re.range "0" "9")) (str.to_re "\u{a}")))))) +(assert (not (str.in_re X (re.++ (str.to_re "//jdb/inf.php?id=") ((_ re.loop 32 32) (re.union (re.range "a" "f") (re.range "0" "9"))) (str.to_re "/Ui\u{a}"))))) +(assert (not (str.in_re X (re.++ (re.* (re.opt (re.range "0" "9"))) (re.opt (re.++ (str.to_re ".") (re.union ((_ re.loop 1 1) (re.range "0" "9")) ((_ re.loop 2 2) (re.range "0" "9"))))) (str.to_re "\u{a}"))))) +(check-sat) + +(exit) diff --git a/benchmarks/instance14382.smt2 b/benchmarks/instance14382.smt2 new file mode 100644 index 000000000..72c67b77c --- /dev/null +++ b/benchmarks/instance14382.smt2 @@ -0,0 +1,21 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_S) +(set-info :source | +Generated by: Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel Day, Dirk Nowotka, Vijay Ganesh, Zhengyang Lu +Generated on: 2020-10-01 +Description: Translated from a collection of real-world regex queries, AutomataArk, collected by Loris D’Antoni and Fang Wang: https://github.com/lorisdanto/automatark +Application: Evaluate solvers on real-world regex queries +Target solver: Z3str3RE, CVC4, OSTRICH, Z3seq, Z3str3, Z3-Trau +Publications: Berzish, M., Kulczynski, M., Mora, F., Manea, F., Day, J. D., Nowotka, D., & Ganesh, V. (2021, July). An SMT solver for regular expressions and linear arithmetic over string length. In CAV 2021. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "industrial") +(set-info :status unsat) + +(declare-const X String) +(assert (str.in_re X (re.++ (str.to_re "~/") (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z") (str.to_re "_")) (re.* (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z") (str.to_re "/") (str.to_re "_") (str.to_re "-"))) (str.to_re ".") (re.+ (re.union (re.range "0" "9") (re.range "a" "z") (re.range "A" "Z") (str.to_re "_") (str.to_re "-"))) (str.to_re "\u{a}")))) +(assert (str.in_re X (re.++ (re.opt (str.to_re "-")) (re.opt (str.to_re ",")) (re.union (re.++ ((_ re.loop 1 3) (re.range "0" "9")) (re.* (re.++ (str.to_re ".") ((_ re.loop 3 3) (re.range "0" "9"))))) (re.+ (re.range "0" "9"))) (re.opt (re.++ (str.to_re ",") ((_ re.loop 2 2) (re.range "0" "9")))) (str.to_re "\u{a}")))) +(assert (not (str.in_re X (re.++ (re.union (str.to_re "big5") (re.++ (str.to_re "euc") (re.union (str.to_re "kr") (str.to_re "jpms"))) (str.to_re "binary") (str.to_re "greek") (str.to_re "tis620") (str.to_re "hebrew") (str.to_re "ascii") (str.to_re "swe7") (re.++ (str.to_re "koi8") (re.union (str.to_re "r") (str.to_re "u"))) (re.++ (re.union (str.to_re "u") (str.to_re "keyb")) (str.to_re "cs2")) (re.++ (re.union (str.to_re "dec") (str.to_re "hp") (str.to_re "utf") (str.to_re "geostd") (str.to_re "armscii")) (str.to_re "8")) (re.++ (str.to_re "gb") (re.union (str.to_re "k") (str.to_re "2312"))) (re.++ (str.to_re "cp") (re.union (re.++ (str.to_re "8") (re.union (re.++ (str.to_re "5") (re.union (str.to_re "0") (str.to_re "2"))) (str.to_re "66"))) (str.to_re "932") (re.++ (str.to_re "125") (re.union (str.to_re "0") (str.to_re "1") (str.to_re "6") (str.to_re "7"))))) (re.++ (str.to_re "latin") (re.union (str.to_re "1") (str.to_re "2") (str.to_re "5") (str.to_re "7"))) (re.++ (re.union (str.to_re "u") (str.to_re "s")) (str.to_re "jis")) (re.++ (str.to_re "mac") (re.union (str.to_re "ce") (str.to_re "roman")))) (str.to_re "\u{a}"))))) +(check-sat) + +(exit) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 047c5f5f1..9f60d5be7 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -43,6 +43,10 @@ namespace seq { void derive::reset() { m_cache.reset(); m_top_cache.reset(); + m_union_cache.reset(); + m_inter_cache.reset(); + m_concat_cache.reset(); + m_complement_cache.reset(); m_trail.reset(); } @@ -573,6 +577,22 @@ namespace seq { } expr_ref derive::mk_union(expr* a, expr* b) { + // Check op cache + expr* cached = nullptr; + if (m_union_cache.find(a, b, cached)) + return expr_ref(cached, m); + + expr_ref result = mk_union_core(a, b); + + // Store in cache + m_union_cache.insert(a, b, result); + m_trail.push_back(a); + m_trail.push_back(b); + m_trail.push_back(result); + return result; + } + + expr_ref derive::mk_union_core(expr* a, expr* b) { // Identity / annihilator if (a == b) return expr_ref(a, m); if (re().is_empty(a)) return expr_ref(b, m); @@ -606,16 +626,29 @@ namespace seq { return mk_ite(c1, then_br, else_br); } - // ITE hoisting: ite(c, t, e) ∪ r = ite(c, t ∪ r, e ∪ r) + // Conservative ITE hoisting via subsumption: + // Only hoist when at least one branch simplifies by is_subset. if (m.is_ite(a, c1, t1, e1)) { - expr_ref then_br = mk_union(t1, b); - expr_ref else_br = mk_union(e1, b); - return mk_ite(c1, then_br, else_br); + bool t1_sub_b = is_subset(t1, b); // t1 ∪ b = b + bool b_sub_t1 = is_subset(b, t1); // t1 ∪ b = t1 + bool e1_sub_b = is_subset(e1, b); // e1 ∪ b = b + bool b_sub_e1 = is_subset(b, e1); // e1 ∪ b = e1 + if (t1_sub_b || b_sub_t1 || e1_sub_b || b_sub_e1) { + expr_ref then_br = t1_sub_b ? expr_ref(b, m) : b_sub_t1 ? expr_ref(t1, m) : mk_union(t1, b); + expr_ref else_br = e1_sub_b ? expr_ref(b, m) : b_sub_e1 ? expr_ref(e1, m) : mk_union(e1, b); + return mk_ite(c1, then_br, else_br); + } } if (m.is_ite(b, c2, t2, e2)) { - expr_ref then_br = mk_union(a, t2); - expr_ref else_br = mk_union(a, e2); - return mk_ite(c2, then_br, else_br); + bool t2_sub_a = is_subset(t2, a); // a ∪ t2 = a + bool a_sub_t2 = is_subset(a, t2); // a ∪ t2 = t2 + bool e2_sub_a = is_subset(e2, a); // a ∪ e2 = a + bool a_sub_e2 = is_subset(a, e2); // a ∪ e2 = e2 + if (t2_sub_a || a_sub_t2 || e2_sub_a || a_sub_e2) { + expr_ref then_br = t2_sub_a ? expr_ref(a, m) : a_sub_t2 ? expr_ref(t2, m) : mk_union(a, t2); + expr_ref else_br = e2_sub_a ? expr_ref(a, m) : a_sub_e2 ? expr_ref(e2, m) : mk_union(a, e2); + return mk_ite(c2, then_br, else_br); + } } // ACI: flatten, sort, deduplicate @@ -647,6 +680,22 @@ namespace seq { } expr_ref derive::mk_inter(expr* a, expr* b) { + // Check op cache + expr* cached = nullptr; + if (m_inter_cache.find(a, b, cached)) + return expr_ref(cached, m); + + expr_ref result = mk_inter_core(a, b); + + // Store in cache + m_inter_cache.insert(a, b, result); + m_trail.push_back(a); + m_trail.push_back(b); + m_trail.push_back(result); + return result; + } + + expr_ref derive::mk_inter_core(expr* a, expr* b) { // Identity / annihilator if (a == b) return expr_ref(a, m); if (re().is_empty(a)) return expr_ref(a, m); @@ -680,16 +729,24 @@ namespace seq { return mk_ite(c1, then_br, else_br); } - // ITE hoisting: ite(c, t, e) ∩ r = ite(c, t ∩ r, e ∩ r) - if (m.is_ite(a, c1, t1, e1)) { - expr_ref then_br = mk_inter(t1, b); - expr_ref else_br = mk_inter(e1, b); - return mk_ite(c1, then_br, else_br); - } - if (m.is_ite(b, c2, t2, e2)) { - expr_ref then_br = mk_inter(a, t2); - expr_ref else_br = mk_inter(a, e2); - return mk_ite(c2, then_br, else_br); + // ITE hoisting for intersection with depth bound. + // Unconditional hoisting needed for re.inter/re.diff/re.comp patterns, + // but bounded to prevent exponential blowup on union-heavy patterns. + if (m_inter_hoist_depth < m_max_inter_hoist_depth) { + if (m.is_ite(a, c1, t1, e1)) { + m_inter_hoist_depth++; + expr_ref then_br = mk_inter(t1, b); + expr_ref else_br = mk_inter(e1, b); + m_inter_hoist_depth--; + return mk_ite(c1, then_br, else_br); + } + if (m.is_ite(b, c2, t2, e2)) { + m_inter_hoist_depth++; + expr_ref then_br = mk_inter(a, t2); + expr_ref else_br = mk_inter(a, e2); + m_inter_hoist_depth--; + return mk_ite(c2, then_br, else_br); + } } // ACI: flatten, sort, deduplicate @@ -763,6 +820,21 @@ namespace seq { } expr_ref derive::mk_complement(expr* a) { + // Check op cache + expr* cached = nullptr; + if (m_complement_cache.find(a, cached)) + return expr_ref(cached, m); + + expr_ref result = mk_complement_core(a); + + // Store in cache + m_complement_cache.insert(a, result); + m_trail.push_back(a); + m_trail.push_back(result); + return result; + } + + expr_ref derive::mk_complement_core(expr* a) { // ~~r → r expr* r = nullptr; if (re().is_complement(a, r)) @@ -952,6 +1024,22 @@ namespace seq { // ------------------------------------------------------- expr_ref derive::mk_deriv_concat(expr* d, expr* tail) { + // Check op cache + expr* cached = nullptr; + if (m_concat_cache.find(d, tail, cached)) + return expr_ref(cached, m); + + expr_ref result = mk_deriv_concat_core(d, tail); + + // Store in cache + m_concat_cache.insert(d, tail, result); + m_trail.push_back(d); + m_trail.push_back(tail); + m_trail.push_back(result); + return result; + } + + expr_ref derive::mk_deriv_concat_core(expr* d, expr* tail) { expr_ref _d(d, m), _tail(tail, m); expr* c, * t, * e; @@ -1173,7 +1261,7 @@ namespace seq { return l_undef; } - std::pair derive::simplify_ite_rec(path_t& path, intervals_t& intervals, expr* c, expr* t, expr* e) { + std::pair derive::simplify_ite_rec(path_t& path, intervals_t& intervals, expr* c, expr* t, expr* e, unsigned depth) { auto sz = path.size(); auto saved_intervals = intervals; @@ -1181,7 +1269,7 @@ namespace seq { lbool path_val = push_path(path, c, false); if (path_val != l_undef) { path.shrink(sz); - expr_ref r = simplify_ite_rec(path, intervals, path_val == l_true ? t : e); + expr_ref r = simplify_ite_rec(path, intervals, path_val == l_true ? t : e, depth); return { r, r }; } @@ -1189,11 +1277,12 @@ namespace seq { if (intv_val != l_undef) { path.shrink(sz); intervals = saved_intervals; - expr_ref r = simplify_ite_rec(path, intervals, intv_val == l_true ? t : e); + expr_ref r = simplify_ite_rec(path, intervals, intv_val == l_true ? t : e, depth); return { r, r }; } - expr_ref st = simplify_ite_rec(path, intervals, t); + // Then-branch increases depth + expr_ref st = simplify_ite_rec(path, intervals, t, depth + 1); path.shrink(sz); intervals = saved_intervals; @@ -1201,7 +1290,7 @@ namespace seq { path_val = push_path(path, c, true); if (path_val != l_undef) { path.shrink(sz); - expr_ref r = simplify_ite_rec(path, intervals, path_val == l_true ? e : t); + expr_ref r = simplify_ite_rec(path, intervals, path_val == l_true ? e : t, depth); return { r, r }; } @@ -1209,11 +1298,12 @@ namespace seq { if (intv_val != l_undef) { path.shrink(sz); intervals = saved_intervals; - expr_ref r = simplify_ite_rec(path, intervals, intv_val == l_true ? e : t); + expr_ref r = simplify_ite_rec(path, intervals, intv_val == l_true ? e : t, depth); return { r, r }; } - expr_ref se = simplify_ite_rec(path, intervals, e); + // Else-branch does NOT increase depth (covers disjoint cases) + expr_ref se = simplify_ite_rec(path, intervals, e, depth); path.shrink(sz); intervals = saved_intervals; return { st, se }; @@ -1231,27 +1321,28 @@ namespace seq { path_t path; intervals_t intervals; intervals.push_back(std::make_pair(0u, u().max_char())); - auto [st, se] = simplify_ite_rec(path, intervals, c, t, e); + auto [st, se] = simplify_ite_rec(path, intervals, c, t, e, 0); return mk_ite(c, st, se); } - expr_ref derive::simplify_ite_rec(path_t& path, intervals_t& intervals, expr* d) { + expr_ref derive::simplify_ite_rec(path_t& path, intervals_t& intervals, expr* d, unsigned depth) { expr* c, * t, * e; if (!m.is_ite(d, c, t, e)) return expr_ref(d, m); + // Depth limit reached — return without further simplification + if (depth >= m_max_simp_depth) + return expr_ref(d, m); + // Try to evaluate c directly (handles trivially true/false conditions) lbool cond_val = eval_cond(c); - if (cond_val == l_true) return simplify_ite_rec(path, intervals, t); - if (cond_val == l_false) return simplify_ite_rec(path, intervals, e); + if (cond_val == l_true) return simplify_ite_rec(path, intervals, t, depth); + if (cond_val == l_false) return simplify_ite_rec(path, intervals, e, depth); // Cannot simplify c: recurse into branches with extended paths // push_path and push_intervals will check subsumption/contradiction - auto [st, se] = simplify_ite_rec(path, intervals, c, t, e); + auto [st, se] = simplify_ite_rec(path, intervals, c, t, e, depth); return mk_ite(c, st, se); } -} - - - +} \ No newline at end of file diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index 0c7961ff1..122619809 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/src/ast/rewriter/seq_derive.h @@ -59,10 +59,24 @@ namespace seq { obj_pair_map m_top_cache; // post-simplify cache expr_ref_vector m_trail; // pin cached results + // Op cache for ITE-hoisting operations (union, inter, concat, complement) + obj_pair_map m_union_cache; + obj_pair_map m_inter_cache; + obj_pair_map m_concat_cache; + obj_map m_complement_cache; + // Depth limiting unsigned m_depth { 0 }; static const unsigned m_max_depth = 512; + // Simplify ITE recursion depth limit + unsigned m_simp_depth { 0 }; + static const unsigned m_max_simp_depth = 8; + + // Intersection ITE hoisting depth limit + unsigned m_inter_hoist_depth { 0 }; + static const unsigned m_max_inter_hoist_depth = 4; + seq_util::rex& re() { return m_util.re; } seq_util& u() { return m_util; } @@ -83,9 +97,12 @@ namespace seq { // Smart constructors with simplification and ACI canonicalization expr_ref mk_union(expr* a, expr* b); + expr_ref mk_union_core(expr* a, expr* b); expr_ref mk_inter(expr* a, expr* b); + expr_ref mk_inter_core(expr* a, expr* b); expr_ref mk_concat(expr* a, expr* b); expr_ref mk_complement(expr* a); + expr_ref mk_complement_core(expr* a); expr_ref mk_ite(expr* c, expr* t, expr* e); // Flatten and sort for ACI normal form @@ -104,6 +121,7 @@ namespace seq { // Distribute concatenation through ITE/union in derivative expr_ref mk_deriv_concat(expr* d, expr* tail); + expr_ref mk_deriv_concat_core(expr* d, expr* tail); // Extract head character and tail from a sequence expression bool get_head_tail(expr* s1, expr* s2, expr_ref& hd, expr_ref& tl); @@ -120,8 +138,8 @@ namespace seq { // Simplify ITE conditions w.r.t. m_ele and path knowledge expr_ref simplify_ite(expr* d); - expr_ref simplify_ite_rec(path_t& path, intervals_t& intervals, expr* d); - std::pair simplify_ite_rec(path_t& path, intervals_t& intervals, expr* c, expr* t, expr* e); + expr_ref simplify_ite_rec(path_t& path, intervals_t& intervals, expr* d, unsigned depth); + std::pair simplify_ite_rec(path_t& path, intervals_t& intervals, expr* c, expr* t, expr* e, unsigned depth); lbool push_path(path_t& path, expr* c, bool sign); lbool push_intervals(intervals_t& intervals, expr* c, bool sign); lbool eval_cond(expr* cond);