blob: aa2ddb2a3abe5bbea98e519525e471a22ad7f0da (
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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --strings-exp
(set-logic S)
(set-option :sygus-rec-fun true)
(set-option :e-matching false)
(define-sort Rex () RegLan)
;SyGuS Grammar Definition.
(synth-fun phi () Rex
((<R> Rex))
((<R> Rex (
; alphabets
(str.to_re "r") ; r = request
(str.to_re "g") ; g = grant
(str.to_re "e") ; e = empty
(str.to_re "b") ; b = request, grant
; (re.none <R>)
; (re.all <R>)
; CHOICE
(re.union <R> <R>)
; CONCATENATION
(re.++ <R> <R>)
; INTERSECTION
(re.inter <R> <R>)
; STAR
(re.* <R>)
; PLUS
(re.+ <R>)
; Complement / Don't work
(re.comp <R>)
; Difference / Don't work
(re.diff <R> <R>)
(re.opt <R>)
)))
)
(define-fun w1() String "ee")
(constraint (str.in_re w1 phi))
(define-fun n1() String "bbegre")
(constraint (str.in_re n1 (re.comp phi)))
(check-synth)
|
