data/sygus/phone-2-long-repeat.sl

(set-logic SLIA)
 
(synth-fun f ((name String)) String
    ((Start String (ntString))
     (ntString String (name " "
                       (str.++ ntString ntString)
                       (str.replace ntString ntString ntString)
                       (str.at ntString ntInt)
                       (int.to.str ntInt)
                       (str.substr ntString ntInt ntInt)))
      (ntInt Int (0 1 2 3 4 5
                  (+ ntInt ntInt)
                  (- ntInt ntInt)
                  (str.len ntString)
                  (str.to.int ntString)
                  (str.indexof ntString ntString ntInt)))
      (ntBool Bool (true false
                    (str.prefixof ntString ntString)
                    (str.suffixof ntString ntString)
                    (str.contains ntString ntString)))))


(declare-var name String)

(constraint (= (f "938-242-504") "504"))
(constraint (= (f "938-242-504") "504"))
(constraint (= (f "938-242-504") "504"))
(constraint (= (f "308-916-545") "545"))
(constraint (= (f "308-916-545") "545"))
(constraint (= (f "308-916-545") "545"))
(constraint (= (f "623-599-749") "749"))
(constraint (= (f "623-599-749") "749"))
(constraint (= (f "623-599-749") "749"))
(constraint (= (f "981-424-843") "843"))
(constraint (= (f "981-424-843") "843"))
(constraint (= (f "981-424-843") "843"))
(constraint (= (f "118-980-214") "214"))
(constraint (= (f "118-980-214") "214"))
(constraint (= (f "118-980-214") "214"))
(constraint (= (f "244-655-094") "094"))
(constraint (= (f "244-655-094") "094"))
(constraint (= (f "244-655-094") "094"))
(constraint (= (f "830-941-991") "991"))
(constraint (= (f "830-941-991") "991"))
(constraint (= (f "830-941-991") "991"))
(constraint (= (f "911-186-562") "562"))
(constraint (= (f "911-186-562") "562"))
(constraint (= (f "911-186-562") "562"))
(constraint (= (f "002-500-200") "200"))
(constraint (= (f "002-500-200") "200"))
(constraint (= (f "002-500-200") "200"))
(constraint (= (f "113-860-034") "034"))
(constraint (= (f "113-860-034") "034"))
(constraint (= (f "113-860-034") "034"))
(constraint (= (f "457-622-959") "959"))
(constraint (= (f "457-622-959") "959"))
(constraint (= (f "457-622-959") "959"))
(constraint (= (f "986-722-311") "311"))
(constraint (= (f "986-722-311") "311"))
(constraint (= (f "986-722-311") "311"))
(constraint (= (f "110-170-771") "771"))
(constraint (= (f "110-170-771") "771"))
(constraint (= (f "110-170-771") "771"))
(constraint (= (f "469-610-118") "118"))
(constraint (= (f "469-610-118") "118"))
(constraint (= (f "469-610-118") "118"))
(constraint (= (f "817-925-247") "247"))
(constraint (= (f "817-925-247") "247"))
(constraint (= (f "817-925-247") "247"))
(constraint (= (f "256-899-439") "439"))
(constraint (= (f "256-899-439") "439"))
(constraint (= (f "256-899-439") "439"))
(constraint (= (f "886-911-726") "726"))
(constraint (= (f "886-911-726") "726"))
(constraint (= (f "886-911-726") "726"))
(constraint (= (f "562-950-358") "358"))
(constraint (= (f "562-950-358") "358"))
(constraint (= (f "562-950-358") "358"))
(constraint (= (f "693-049-588") "588"))
(constraint (= (f "693-049-588") "588"))
(constraint (= (f "693-049-588") "588"))
(constraint (= (f "840-503-234") "234"))
(constraint (= (f "840-503-234") "234"))
(constraint (= (f "840-503-234") "234"))
(constraint (= (f "698-815-340") "340"))
(constraint (= (f "698-815-340") "340"))
(constraint (= (f "698-815-340") "340"))
(constraint (= (f "498-808-434") "434"))
(constraint (= (f "498-808-434") "434"))
(constraint (= (f "498-808-434") "434"))
(constraint (= (f "329-545-000") "000"))
(constraint (= (f "329-545-000") "000"))
(constraint (= (f "329-545-000") "000"))
(constraint (= (f "380-281-597") "597"))
(constraint (= (f "380-281-597") "597"))
(constraint (= (f "380-281-597") "597"))
(constraint (= (f "332-395-493") "493"))
(constraint (= (f "332-395-493") "493"))
(constraint (= (f "332-395-493") "493"))
(constraint (= (f "251-903-028") "028"))
(constraint (= (f "251-903-028") "028"))
(constraint (= (f "251-903-028") "028"))
(constraint (= (f "176-090-894") "894"))
(constraint (= (f "176-090-894") "894"))
(constraint (= (f "176-090-894") "894"))
(constraint (= (f "336-611-100") "100"))
(constraint (= (f "336-611-100") "100"))
(constraint (= (f "336-611-100") "100"))
(constraint (= (f "416-390-647") "647"))
(constraint (= (f "416-390-647") "647"))
(constraint (= (f "416-390-647") "647"))
(constraint (= (f "019-430-596") "596"))
(constraint (= (f "019-430-596") "596"))
(constraint (= (f "019-430-596") "596"))
(constraint (= (f "960-659-771") "771"))
(constraint (= (f "960-659-771") "771"))
(constraint (= (f "960-659-771") "771"))
(constraint (= (f "475-505-007") "007"))
(constraint (= (f "475-505-007") "007"))
(constraint (= (f "475-505-007") "007"))
(constraint (= (f "424-069-886") "886"))
(constraint (= (f "424-069-886") "886"))
(constraint (= (f "424-069-886") "886"))
(constraint (= (f "941-102-117") "117"))
(constraint (= (f "941-102-117") "117"))
(constraint (= (f "941-102-117") "117"))
(constraint (= (f "331-728-008") "008"))
(constraint (= (f "331-728-008") "008"))
(constraint (= (f "331-728-008") "008"))
(constraint (= (f "487-726-198") "198"))
(constraint (= (f "487-726-198") "198"))
(constraint (= (f "487-726-198") "198"))
(constraint (= (f "612-419-942") "942"))
(constraint (= (f "612-419-942") "942"))
(constraint (= (f "612-419-942") "942"))
(constraint (= (f "594-741-346") "346"))
(constraint (= (f "594-741-346") "346"))
(constraint (= (f "594-741-346") "346"))
(constraint (= (f "320-984-742") "742"))
(constraint (= (f "320-984-742") "742"))
(constraint (= (f "320-984-742") "742"))
(constraint (= (f "060-919-361") "361"))
(constraint (= (f "060-919-361") "361"))
(constraint (= (f "060-919-361") "361"))
(constraint (= (f "275-536-998") "998"))
(constraint (= (f "275-536-998") "998"))
(constraint (= (f "275-536-998") "998"))
(constraint (= (f "548-835-065") "065"))
(constraint (= (f "548-835-065") "065"))
(constraint (= (f "548-835-065") "065"))
(constraint (= (f "197-485-507") "507"))
(constraint (= (f "197-485-507") "507"))
(constraint (= (f "197-485-507") "507"))
(constraint (= (f "455-776-949") "949"))
(constraint (= (f "455-776-949") "949"))
(constraint (= (f "455-776-949") "949"))
(constraint (= (f "085-421-340") "340"))
(constraint (= (f "085-421-340") "340"))
(constraint (= (f "085-421-340") "340"))
(constraint (= (f "785-713-099") "099"))
(constraint (= (f "785-713-099") "099"))
(constraint (= (f "785-713-099") "099"))
(constraint (= (f "426-712-861") "861"))
(constraint (= (f "426-712-861") "861"))
(constraint (= (f "426-712-861") "861"))
(constraint (= (f "386-994-906") "906"))
(constraint (= (f "386-994-906") "906"))
(constraint (= (f "386-994-906") "906"))
(constraint (= (f "918-304-840") "840"))
(constraint (= (f "918-304-840") "840"))
(constraint (= (f "918-304-840") "840"))
(constraint (= (f "247-153-598") "598"))
(constraint (= (f "247-153-598") "598"))
(constraint (= (f "247-153-598") "598"))
(constraint (= (f "075-497-069") "069"))
(constraint (= (f "075-497-069") "069"))
(constraint (= (f "075-497-069") "069"))
(constraint (= (f "140-726-583") "583"))
(constraint (= (f "140-726-583") "583"))
(constraint (= (f "140-726-583") "583"))
(constraint (= (f "049-413-248") "248"))
(constraint (= (f "049-413-248") "248"))
(constraint (= (f "049-413-248") "248"))
(constraint (= (f "977-386-462") "462"))
(constraint (= (f "977-386-462") "462"))
(constraint (= (f "977-386-462") "462"))
(constraint (= (f "058-272-455") "455"))
(constraint (= (f "058-272-455") "455"))
(constraint (= (f "058-272-455") "455"))
(constraint (= (f "428-629-927") "927"))
(constraint (= (f "428-629-927") "927"))
(constraint (= (f "428-629-927") "927"))
(constraint (= (f "449-122-191") "191"))
(constraint (= (f "449-122-191") "191"))
(constraint (= (f "449-122-191") "191"))
(constraint (= (f "568-759-670") "670"))
(constraint (= (f "568-759-670") "670"))
(constraint (= (f "568-759-670") "670"))
(constraint (= (f "312-846-053") "053"))
(constraint (= (f "312-846-053") "053"))
(constraint (= (f "312-846-053") "053"))
(constraint (= (f "943-037-297") "297"))
(constraint (= (f "943-037-297") "297"))
(constraint (= (f "943-037-297") "297"))
(constraint (= (f "014-270-177") "177"))
(constraint (= (f "014-270-177") "177"))
(constraint (= (f "014-270-177") "177"))
(constraint (= (f "658-877-878") "878"))
(constraint (= (f "658-877-878") "878"))
(constraint (= (f "658-877-878") "878"))
(constraint (= (f "888-594-038") "038"))
(constraint (= (f "888-594-038") "038"))
(constraint (= (f "888-594-038") "038"))
(constraint (= (f "232-253-254") "254"))
(constraint (= (f "232-253-254") "254"))
(constraint (= (f "232-253-254") "254"))
(constraint (= (f "308-722-292") "292"))
(constraint (= (f "308-722-292") "292"))
(constraint (= (f "308-722-292") "292"))
(constraint (= (f "342-145-742") "742"))
(constraint (= (f "342-145-742") "742"))
(constraint (= (f "342-145-742") "742"))
(constraint (= (f "568-181-515") "515"))
(constraint (= (f "568-181-515") "515"))
(constraint (= (f "568-181-515") "515"))
(constraint (= (f "300-140-756") "756"))
(constraint (= (f "300-140-756") "756"))
(constraint (= (f "300-140-756") "756"))
(constraint (= (f "099-684-216") "216"))
(constraint (= (f "099-684-216") "216"))
(constraint (= (f "099-684-216") "216"))
(constraint (= (f "575-296-621") "621"))
(constraint (= (f "575-296-621") "621"))
(constraint (= (f "575-296-621") "621"))
(constraint (= (f "994-443-794") "794"))
(constraint (= (f "994-443-794") "794"))
(constraint (= (f "994-443-794") "794"))
(constraint (= (f "400-334-692") "692"))
(constraint (= (f "400-334-692") "692"))
(constraint (= (f "400-334-692") "692"))
(constraint (= (f "684-711-883") "883"))
(constraint (= (f "684-711-883") "883"))
(constraint (= (f "684-711-883") "883"))
(constraint (= (f "539-636-358") "358"))
(constraint (= (f "539-636-358") "358"))
(constraint (= (f "539-636-358") "358"))
(constraint (= (f "009-878-919") "919"))
(constraint (= (f "009-878-919") "919"))
(constraint (= (f "009-878-919") "919"))
(constraint (= (f "919-545-701") "701"))
(constraint (= (f "919-545-701") "701"))
(constraint (= (f "919-545-701") "701"))
(constraint (= (f "546-399-239") "239"))
(constraint (= (f "546-399-239") "239"))
(constraint (= (f "546-399-239") "239"))
(constraint (= (f "993-608-757") "757"))
(constraint (= (f "993-608-757") "757"))
(constraint (= (f "993-608-757") "757"))
(constraint (= (f "107-652-845") "845"))
(constraint (= (f "107-652-845") "845"))
(constraint (= (f "107-652-845") "845"))
(constraint (= (f "206-805-793") "793"))
(constraint (= (f "206-805-793") "793"))
(constraint (= (f "206-805-793") "793"))
(constraint (= (f "198-857-684") "684"))
(constraint (= (f "198-857-684") "684"))
(constraint (= (f "198-857-684") "684"))
(constraint (= (f "912-827-430") "430"))
(constraint (= (f "912-827-430") "430"))
(constraint (= (f "912-827-430") "430"))
(constraint (= (f "560-951-766") "766"))
(constraint (= (f "560-951-766") "766"))
(constraint (= (f "560-951-766") "766"))
(constraint (= (f "142-178-290") "290"))
(constraint (= (f "142-178-290") "290"))
(constraint (= (f "142-178-290") "290"))
(constraint (= (f "732-196-946") "946"))
(constraint (= (f "732-196-946") "946"))
(constraint (= (f "732-196-946") "946"))
(constraint (= (f "963-875-745") "745"))
(constraint (= (f "963-875-745") "745"))
(constraint (= (f "963-875-745") "745"))
(constraint (= (f "881-865-867") "867"))
(constraint (= (f "881-865-867") "867"))
(constraint (= (f "881-865-867") "867"))
(constraint (= (f "234-686-715") "715"))
(constraint (= (f "234-686-715") "715"))
(constraint (= (f "234-686-715") "715"))
(constraint (= (f "720-330-583") "583"))
(constraint (= (f "720-330-583") "583"))
(constraint (= (f "720-330-583") "583"))
(constraint (= (f "593-065-126") "126"))
(constraint (= (f "593-065-126") "126"))
(constraint (= (f "593-065-126") "126"))
(constraint (= (f "671-778-064") "064"))
(constraint (= (f "671-778-064") "064"))
(constraint (= (f "671-778-064") "064"))
(constraint (= (f "252-029-036") "036"))
(constraint (= (f "252-029-036") "036"))
(constraint (= (f "252-029-036") "036"))
(constraint (= (f "700-322-036") "036"))
(constraint (= (f "700-322-036") "036"))
(constraint (= (f "700-322-036") "036"))
(constraint (= (f "882-587-473") "473"))
(constraint (= (f "882-587-473") "473"))
(constraint (= (f "882-587-473") "473"))
(constraint (= (f "964-134-953") "953"))
(constraint (= (f "964-134-953") "953"))
(constraint (= (f "964-134-953") "953"))
(constraint (= (f "038-300-876") "876"))
(constraint (= (f "038-300-876") "876"))
(constraint (= (f "038-300-876") "876"))
(constraint (= (f "158-894-947") "947"))
(constraint (= (f "158-894-947") "947"))
(constraint (= (f "158-894-947") "947"))
(constraint (= (f "757-454-374") "374"))
(constraint (= (f "757-454-374") "374"))
(constraint (= (f "757-454-374") "374"))
(constraint (= (f "872-513-190") "190"))
(constraint (= (f "872-513-190") "190"))
(constraint (= (f "872-513-190") "190"))
(constraint (= (f "566-086-726") "726"))
(constraint (= (f "566-086-726") "726"))
(constraint (= (f "566-086-726") "726"))
(constraint (= (f "938-242-504") "504"))
(constraint (= (f "308-916-545") "545"))
(constraint (= (f "623-599-749") "749"))
(constraint (= (f "981-424-843") "843"))
(constraint (= (f "118-980-214") "214"))
(constraint (= (f "244-655-094") "094"))
(constraint (= (f "830-941-991") "991"))
(constraint (= (f "911-186-562") "562"))
(constraint (= (f "002-500-200") "200"))
(constraint (= (f "113-860-034") "034"))
(constraint (= (f "457-622-959") "959"))
(constraint (= (f "986-722-311") "311"))
(constraint (= (f "110-170-771") "771"))
(constraint (= (f "469-610-118") "118"))
(constraint (= (f "817-925-247") "247"))
(constraint (= (f "256-899-439") "439"))
(constraint (= (f "886-911-726") "726"))
(constraint (= (f "562-950-358") "358"))
(constraint (= (f "693-049-588") "588"))
(constraint (= (f "840-503-234") "234"))
(constraint (= (f "698-815-340") "340"))
(constraint (= (f "498-808-434") "434"))
(constraint (= (f "329-545-000") "000"))
(constraint (= (f "380-281-597") "597"))
(constraint (= (f "332-395-493") "493"))
(constraint (= (f "251-903-028") "028"))
(constraint (= (f "176-090-894") "894"))
(constraint (= (f "336-611-100") "100"))
(constraint (= (f "416-390-647") "647"))
(constraint (= (f "019-430-596") "596"))
(constraint (= (f "960-659-771") "771"))
(constraint (= (f "475-505-007") "007"))
(constraint (= (f "424-069-886") "886"))
(constraint (= (f "941-102-117") "117"))
(constraint (= (f "331-728-008") "008"))
(constraint (= (f "487-726-198") "198"))
(constraint (= (f "612-419-942") "942"))
(constraint (= (f "594-741-346") "346"))
(constraint (= (f "320-984-742") "742"))
(constraint (= (f "060-919-361") "361"))
(constraint (= (f "275-536-998") "998"))
(constraint (= (f "548-835-065") "065"))
(constraint (= (f "197-485-507") "507"))
(constraint (= (f "455-776-949") "949"))
(constraint (= (f "085-421-340") "340"))
(constraint (= (f "785-713-099") "099"))
(constraint (= (f "426-712-861") "861"))
(constraint (= (f "386-994-906") "906"))
(constraint (= (f "918-304-840") "840"))
(constraint (= (f "247-153-598") "598"))
(constraint (= (f "075-497-069") "069"))
(constraint (= (f "140-726-583") "583"))
(constraint (= (f "049-413-248") "248"))
(constraint (= (f "977-386-462") "462"))
(constraint (= (f "058-272-455") "455"))
(constraint (= (f "428-629-927") "927"))
(constraint (= (f "449-122-191") "191"))
(constraint (= (f "568-759-670") "670"))
(constraint (= (f "312-846-053") "053"))
(constraint (= (f "943-037-297") "297"))
(constraint (= (f "014-270-177") "177"))
(constraint (= (f "658-877-878") "878"))
(constraint (= (f "888-594-038") "038"))
(constraint (= (f "232-253-254") "254"))
(constraint (= (f "308-722-292") "292"))
(constraint (= (f "342-145-742") "742"))
(constraint (= (f "568-181-515") "515"))
(constraint (= (f "300-140-756") "756"))
(constraint (= (f "099-684-216") "216"))
(constraint (= (f "575-296-621") "621"))
(constraint (= (f "994-443-794") "794"))
(constraint (= (f "400-334-692") "692"))
(constraint (= (f "684-711-883") "883"))
(constraint (= (f "539-636-358") "358"))
(constraint (= (f "009-878-919") "919"))
(constraint (= (f "919-545-701") "701"))
(constraint (= (f "546-399-239") "239"))
(constraint (= (f "993-608-757") "757"))
(constraint (= (f "107-652-845") "845"))
(constraint (= (f "206-805-793") "793"))
(constraint (= (f "198-857-684") "684"))
(constraint (= (f "912-827-430") "430"))
(constraint (= (f "560-951-766") "766"))
(constraint (= (f "142-178-290") "290"))
(constraint (= (f "732-196-946") "946"))
(constraint (= (f "963-875-745") "745"))
(constraint (= (f "881-865-867") "867"))
(constraint (= (f "234-686-715") "715"))
(constraint (= (f "720-330-583") "583"))
(constraint (= (f "593-065-126") "126"))
(constraint (= (f "671-778-064") "064"))
(constraint (= (f "252-029-036") "036"))
(constraint (= (f "700-322-036") "036"))
(constraint (= (f "882-587-473") "473"))
(constraint (= (f "964-134-953") "953"))
(constraint (= (f "038-300-876") "876"))
(constraint (= (f "158-894-947") "947"))
(constraint (= (f "757-454-374") "374"))
(constraint (= (f "872-513-190") "190"))
(constraint (= (f "566-086-726") "726"))

(check-synth)