Newer
Older
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
;; The background theory
(set-logic NRA)
(define-fun sqr ((x Real)) Real (* x x))
;(define-fun sqr ((x Real)) Real (ite (>= x 0) x (- x) ))
(define-fun error ((x Real)) Real (ite (> x 0) x (* (- 1) x) ) )
(define-fun transitionX ((x Real) (xP Real)) Real
(ite (> xP 0) (- x 1) (ite (= xP 0) x (+ x 1)))
)
(define-fun transitionY ((y Real) (yP Real)) Real
(ite (> yP 0) (- y 1) (ite (= yP 0) y (+ y 1)))
)
(synth-fun inCircle ((x Real) (y Real) (xP Real) (yP Real)) Bool
;; Declare the non-terminals that would be used in the grammar
( (B Bool) (R Real) (C Real))
(
(B Bool ( (<= R (sqr C)) ))
(R Real (
(+ (sqr (- xP (+ (* C x) (* C y) 0 ) ))
(sqr (- yP (+ (* C x) (* C y) 0 ) ))
)
)
)
(C Real ( (Constant Real) )
)
)
)
; (declare-var xx Real)
; (declare-var yy Real)
; (declare-var xxP Real)
; (declare-var yyP Real)
;; Define the semantic constraints on the function
;; x y x' y'
(constraint (= (inCircle 10 (- 10) 11 (- 11) ) true ) )
(constraint (= (inCircle 10 (- 10) 9 (- 9) ) true ) )
(constraint (= (inCircle 1 1 2 2 ) false) )
;(constraint (= (inCircle 1 1 1.5 2.3 ) true ) )
; (constraint (=>
; (inCircle xx yy xxP yyP )
; (and (<= (error (transitionX xx xxP)) (error xx) )
; (<= (error (transitionX yy yyP)) (error yy) )
; )
; )
; )
(check-synth)
; (define-fun inCircle ((x Real) (y Real) (xP Real) (yP Real)) Bool
; (<= (+ (sqr (- xP (+ (* 1 x) (* 0 y) 0))) (sqr (- yP (+ (* 0 x) (* 1 y) 0)))) (sqr 2)))