Merge pull request #6 from OliverMa1/main

Cyclic Word Equations with Regular Constraints

non-incremental/QF_S/20240318-omark/cloud-service-query-1.smt2

@@ -0,0 +1,42 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Query for Cloud Services
+Target solver: OSTRICH
+Simple word equation with regular constraints.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status sat)
+
+(declare-const V31 String)
+(declare-const V32 String)
+(declare-const V16 String)
+(declare-const V29 String)
+(declare-const V30 String)
+(declare-const V17 String)
+(declare-const k!8 String)
+(declare-const k!7 String)
+(declare-const k!3 String)
+(declare-const V33 String)
+(declare-const V34 String)
+(declare-const V35 String)
+(declare-const V3 String)
+(declare-const V36 String)
+(declare-const V37 String)
+(declare-const V1 String)
+
+(assert  (= (str.++ V31 "@" V32) (str.++ V16 V29 ":" V30 V17)))
+
+(assert  (= (str.++ V29 ":" V30) (str.++ k!8 "G" k!7)))
+
+(assert (= (str.++ V33 "/" V34) (str.++ V1 V31 "@" V32 V3)))
+
+(assert  (= (str.++ V36 "://" V37) (str.++ V33 "/" V34 k!3)))
+
+(assert  (= (str.++ "mongodb://" V35) (str.++ V33 "/" V34 k!3)))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/cloud-service-query-2.smt2

@@ -0,0 +1,45 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Query for Cloud Services
+Target solver: OSTRICH
+Simple word equation with regular constraints.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-const V31 String)
+(declare-const V32 String)
+(declare-const V16 String)
+(declare-const V29 String)
+(declare-const V30 String)
+(declare-const V17 String)
+(declare-const k!8 String)
+(declare-const k!7 String)
+(declare-const k!3 String)
+(declare-const V33 String)
+(declare-const V34 String)
+(declare-const V35 String)
+(declare-const V3 String)
+(declare-const V36 String)
+(declare-const V37 String)
+(declare-const V1 String)
+
+(assert  (= (str.++ V31 "@" V32) (str.++ V16 V29 ":" V30 V17)))
+
+(assert  (= (str.++ V29 ":" V30) (str.++ k!8 "G" k!7)))
+
+(assert (= (str.++ V33 "/" V34) (str.++ V1 V31 "@" V32 V3)))
+
+(assert  (= (str.++ V36 "://" V37) (str.++ V33 "/" V34 k!3)))
+
+(assert  (= (str.++ "mongodb://" V35) (str.++ V33 "/" V34 k!3)))
+
+(assert (str.in_re V31 (re.* (str.to_re "a"))))
+(assert (str.in_re V32 (re.* (str.to_re "b"))))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/cyclic-xy.smt2

@@ -0,0 +1,22 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Cyclic Word equations
+Target solver: OSTRICH
+Simple cyclic word equation with regular constraints.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (= (str.++ y x) (str.++ x y)))
+(assert (str.in_re x (re.union (str.to_re "a") (str.to_re "b"))))
+(assert (str.in_re y (re.union (str.to_re "bab") (str.to_re "aba"))))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-1.smt2

@@ -0,0 +1,26 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Instance of Lyndon-Schuetzenberger theorem
+Target solver: OSTRICH
+This benchmark is based on the Lyndon and Schützenberger theorem on word equations.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun X () String)
+(declare-fun A () String)
+(declare-fun B () String)
+(declare-fun C () String)
+(declare-fun D () String)
+(declare-fun E () String)
+
+(assert (= X (str.++ A B C)))
+(assert (= (str.++ X X) (str.++ A A B B C C)))
+(assert (= (str.++ X X X) (str.++ A A A B B B C C C)))
+(assert (str.in_re C (re.++(str.to_re "b") re.all)))
+(assert (str.in_re B (re.++(str.to_re "a") re.all)))
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-2.smt2

@@ -0,0 +1,27 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Instance of Lyndon-Schuetzenberger theorem
+Target solver: OSTRICH
+This benchmark is based on the Lyndon and Schützenberger theorem on word equations.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun X () String)
+(declare-fun A () String)
+(declare-fun B () String)
+(declare-fun C () String)
+(declare-fun D () String)
+(declare-fun E () String)
+
+(assert (= X (str.++ A B C)))
+(assert (= (str.++ X X) (str.++ A A B B C C)))
+(assert (= (str.++ X X X) (str.++ A A A B B B C C C)))
+(assert (str.in_re B (re.+ (str.to_re "b"))))
+(assert (str.in_re A (re.+ (str.to_re "a"))))
+(check-sat)
+(exit)
+

non-incremental/QF_S/20240318-omark/lyndon-schuetzenberg-3.smt2

@@ -0,0 +1,27 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Instance of Lyndon-Schuetzenberger theorem
+Target solver: OSTRICH
+This benchmark is based on the Lyndon and Schützenberger theorem on word equations.
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun X () String)
+(declare-fun A () String)
+(declare-fun B () String)
+(declare-fun C () String)
+(declare-fun D () String)
+(declare-fun E () String)
+
+(assert (= X (str.++ A B C)))
+(assert (= C (str.++ "b" D)))
+(assert (= B (str.++ "a" E)))
+(assert (= (str.++ X X) (str.++ A A B B C C)))
+(assert (= (str.++ X X X) (str.++ A A A B B B C C C)))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-10.smt2

@@ -0,0 +1,22 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ "2" y x) (str.++ x x "2")))
+(assert (str.in_re x (re.++(str.to_re "2") (re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+(assert (str.in_re y (re.++(str.to_re "2")(re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-2.smt2

@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x z x z)))
+(assert (str.in_re x (re.* (str.to_re "1"))))
+(assert (str.in_re y (re.++ (re.+ (str.to_re "1"))  (re.+ (str.to_re "2")) )))
+(assert (str.in_re z (re.* (str.to_re "2"))))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-3.smt2

@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ "1111" z "1" y x "21111") (str.++ "11" x x "111" z)))
+(assert (str.in_re x (re.++ (re.+ (str.to_re "1"))  (re.+ (str.to_re "2")) )))
+(assert (str.in_re y (re.++ (re.+ (str.to_re "1"))  (re.* (str.to_re "2")) )))
+(assert (str.in_re z (re.++ (re.+ (str.to_re "2"))  (re.* (str.to_re "1")) )))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-4.smt2

@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.+ (str.to_re "1111"))))
+(assert (str.in_re y (str.to_re "11")))
+(assert (str.in_re z (re.+ (str.to_re "111"))))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-5.smt2

@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") re.all)))
+(assert (str.in_re y (re.++(str.to_re "1") re.all)))
+(assert (str.in_re z (re.++(str.to_re "2") re.all)))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-6.smt2

@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") (re.union (str.to_re "1")(str.to_re "2")))))
+(assert (str.in_re y (re.++(str.to_re "1") re.all)))
+(assert (str.in_re z (re.++(str.to_re "2") re.all)))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-7.smt2

@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") re.all)))
+(assert (str.in_re y (re.++(str.to_re "1") re.all)))
+(assert (str.in_re z (str.to_re "2")))
+
+(check-sat)
+(exit)

non-incremental/QF_S/20240318-omark/noodles-unsat-8.smt2

@@ -0,0 +1,24 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_S)
+(set-info :source |
+Generated by: Oliver Markgraf
+Generated on: 2024-03-18
+Application: Word equations + Regular Constraints
+Target solver: OSTRICH
+This benchmark is a derivation from the introduction example in the paper "Word Equations in Synergy with Regular Constraints".
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status unknown)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= (str.++ z y x) (str.++ x x z)))
+(assert (str.in_re x (re.++(str.to_re "2") (re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+(assert (str.in_re y (re.++(str.to_re "1") (re.union (re.* (str.to_re "1"))(re.* (str.to_re "2"))))))
+(assert (str.in_re z (re.++(str.to_re "2") re.all)))
+
+(check-sat)
+(exit)