From 3acf1bd23a8e5973be14e7936806f79a4b816c9d Mon Sep 17 00:00:00 2001 From: Angello Astorga <aastorg2@illinois.edu> Date: Mon, 29 Nov 2021 12:05:51 -0500 Subject: [PATCH] cleaning circle region synth --- circleSygus.sl | 28 ++++------------------------ 1 file changed, 4 insertions(+), 24 deletions(-) diff --git a/circleSygus.sl b/circleSygus.sl index 890e119..8446fa2 100755 --- a/circleSygus.sl +++ b/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) -- GitLab