blob: b4c248de9ee4e3dac0fe00481416a683b12813fc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic SLIA)
(synth-fun P ((x String)) Bool (
(Start Bool (
(str.in.re StartStr StartRL)
))
(StartStr String (
x
(str.++ StartStr StartStr)
))
(StartStrC String (
"A" "B" ""
(str.++ StartStrC StartStrC)))
(StartRL RegLan (
(re.++ StartRLi StartRLi)
(re.inter StartRL StartRL)
(re.union StartRL StartRL)
(re.* StartRLi)
))
(StartRLi RegLan (
(str.to.re StartStrC)
(re.inter StartRLi StartRLi)
(re.union StartRLi StartRLi)
(re.++ StartRLi StartRLi)
(re.* StartRLi)
))
))
(constraint (P "AAAAA"))
(constraint (P "AAA"))
(constraint (P "AA"))
(constraint (not (P "AB")))
(constraint (not (P "B")))
; (str.in.re x (re.* (str.to.re "A"))) is a solution
(check-synth)
|
