blob: 89f112e0af4f3be6562a69920f3a9abdc8a1e34b (
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification
(set-logic LIA)
(synth-fun f1 ((p1 Int) (P1 Int)) Int
((Start Int))
((Start Int (
p1
P1
(- Start Start)
(+ Start Start)
)))
)
(synth-fun f2 ((p1 Int) (P1 Int)) Int
((Start Int))
((Start Int (
p1
P1
(+ Start Start)
)))
)
(synth-fun f3 ((p1 Int) (P1 Int)) Int
((Start Int))
((Start Int (
p1
P1
(- Start Start)
(+ Start Start)
)))
)
(synth-fun f4 ((p1 Int) (P1 Int)) Int
((Start Int))
((Start Int (
p1
P1
(- Start Start)
(+ Start Start)
)))
)
(synth-fun f5 ((p1 Int) (P1 Int)) Int
((Start Int))
((Start Int (
p1
P1
(- Start Start)
(+ Start Start)
)))
)
(synth-fun g1 ((p1 Int) (P1 Int)) Int
((Start Int))
((Start Int (
p1
P1
(- Start Start)
(+ Start Start)
)))
)
(declare-var x Int)
(declare-var y Int)
(constraint (= (+ (f1 x y) (f1 x y)) (f2 x y)))
(constraint (= (- (+ (f1 x y) (f2 x y)) y) (f3 x y)))
(constraint (= (+ (f2 x y) (f2 x y)) (f4 x y)))
(constraint (= (+ (f4 x y) (f1 x y)) (f5 x y)))
(constraint (= (- (f1 x y) y) (g1 x y)))
(check-synth)
;; possible solution
;; f1: y+x+1
;; f2: y+2x+2
;; f3: y+3x+3
;; f4: 4y+4x+4
;; f5: 5y+5x+5
;; g1: x+1
;; g2: y+2
;; g3: y+3
;; g4: 2y+6
;; g5: 3y+x+7
|
