Skip to content
Snippets Groups Projects
circleSygus.sl 1.81 KiB
Newer Older
;; 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)))
)

aastorg2's avatar
aastorg2 committed
(synth-fun inCircle ((x Real) (y Real) (x_p Real) (y_p 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 (
aastorg2's avatar
aastorg2 committed
                    (+  (sqr (- x_p (+ (* C x) (* C y) 0 ) ))
                        (sqr (- y_p (+ (* C x) (* C y) 0 ) ))
aastorg2's avatar
aastorg2 committed
(synth-fun inCircle2 ((x Real) (y Real) (x_p Real) (y_p 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 (- x_p (+ (* C x) (* C y) 0 ) ))
                        (sqr (- y_p (+ (* C x) (* C y) 0 ) ))
                    )
                )
        )
        (C Real ( (Constant Real) )

        )
        

    )

)

(synth-fun inShape ((x Real) (y Real) (x_p Real) (y_p Real)) Bool

        ;; Declare the non-terminals that would be used in the grammar
    ;((B Bool))

    (
        (B Bool ( (inCircle x y x_p y_p ) (inCircle2 x y x_p y_p) )
        )
    )
    

)

;; Define the semantic constraints on the function

aastorg2's avatar
aastorg2 committed
(constraint  (= (inShape 10 (- 10) 11 (- 11) ) true ) )
(constraint  (= (inShape 10 (- 10) 9 (- 9) ) true ) )
(constraint  (= (inShape 1 1 2 2 ) false) )
aastorg2's avatar
aastorg2 committed
(check-synth)