cleaning circle region synth

circleSygus.sl

@@ -40,31 +40,11 @@
 
 
 
-
-; (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 
+(constraint  (= (inCircle 10 (- 10) 11 (- 11) ) true ) )
+(constraint  (= (inCircle 10 (- 10) 9 (- 9) ) true ) )
+(constraint  (= (inCircle 1 1 2 2 ) false) )
 
-; (<= (+ (sqr (- xP (+ (* 1 x) (* 0 y) 0))) (sqr (- yP (+ (* 0 x) (* 1 y) 0)))) (sqr 2)))
+(check-synth)