blob: b7646725dcbf96d956945fc7ab77c92581e46762 (
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
38
39
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic SLIA)
(synth-fun P ((x String)) Bool
((Start Bool) (StartStr String) (StartStrC String) (StartRL RegLan) (StartRLi RegLan)) (
(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)
|
