addind sygus formulation for synthesizing circular region

circleSygus.sl

+;; 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)))
+