blob: 7e32384b38bdc1c9285994fdb21811c2b02d04f8 (
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
89
90
91
92
93
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
(set-logic ALL)
; The environment datatypes
(declare-datatype NVars ((x) (y)))
(declare-datatype Pair ((build (first NVars) (second Int))))
(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
(ite (is-nil env)
(cons (build var value) env)
(ite (= var (first (head env)))
(cons (build var value) (tail env))
(cons (head env) (envStore var value (tail env)))
)
)
)
(define-fun-rec envSelect ((var NVars) (env Env)) Int
(ite (is-nil env)
0
(ite (= var (first (head env)))
(second (head env))
(envSelect var (tail env))
)
)
)
; Syntax for arithmetic expressions
(declare-datatype Aexp
(
(Val (val Int))
(Var (name NVars))
(Add (addL Aexp) (addR Aexp))
(Sub (subL Aexp) (subR Aexp))
)
)
; Function to evaluate arithmetic expressions
(define-fun-rec evalA ((env Env) (a Aexp)) Int
(ite (is-Val a)
(val a)
(envSelect (name a) env)
))
; Syntax for boolean expressions
(declare-datatype Bexp
(
(GTH (geqL Aexp) (geqR Aexp))
)
)
; Function to evaluate boolean expressions
(define-fun-rec evalB ((env Env) (b Bexp)) Bool
(> (evalA env (geqL b)) (evalA env (geqR b)))
)
; Syntax for commands
(declare-datatype Com
(
(Assign (lhs NVars) (rhs Aexp))
(While (wCond Bexp) (wCom Com))
)
)
; Function to evaluate statements
(define-fun-rec evalC ((env Env) (c Com)) Env
(ite (is-Assign c)
(envStore (lhs c) (evalA env (rhs c)) env)
(ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env)
)
)
(synth-fun prog () Com
((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int))
(
(C1 Com ((While B C2)))
(C2 Com ((Assign VX A2)))
(VX NVars (x))
(A1 Aexp ((Var VX)))
(A2 Aexp ((Val I)))
(B Bexp ((GTH A2 A1)))
(I Int (2))
)
)
(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil)))
(check-synth)
|
