;; The background theory 
(set-logic LRA)

(define-fun split ((x Real) (c Real) (then_pred Bool) (e1se_pred Bool)) Bool
    (and (=> (>= x c) then_pred) (=> (<= x c) e1se_pred))
)

(define-fun Abs ((x Real)) Real (ite (>= x 0) x (- x) ))
(define-fun L1_norm ((x1 Real) (x2 Real)) Real (+ (Abs x1) (Abs x2))) ; diamond

(define-fun sqr ((x Real)) Real (* x x))
(define-fun L2_norm ((x1 Real) (x2 Real)) Real (+ (sqr x1) (sqr x2))) ; circle

(define-fun max ((x1 Real) (x2 Real)) Real (ite  (>= x1 x2) x1 x2))
(define-fun Loo_norm ((x1 Real) (x2 Real)) Real (max  (Abs x1) (Abs x2))) ; squares

(synth-fun inShape ((x1 Real) (x2 Real) (x3 Real) (z1 Real) (z2 Real)) Bool
    ;; Declare the non-terminals that would be used in the grammar
    ( (B Bool) (Dist Real) (X Real) (C Real))

    (
        (B Bool (
            false
            (<= Dist C)
            ;(split X C B B)
        ))
        (Dist Real (
            (L1_norm  (- z1 (+ (* C x1) (* C x2) (* C x3)  C) ) (- z2 (+ (* C x1) (* C x2) (* C x3) C)))
            (L2_norm  (- z1 (+ (* C x1) (* C x2) (* C x3) C) ) (- z2 (+ (* C x1) (* C x2) (* C x3) C)))
            (Loo_norm (- z1 (+ (* C x1) (* C x2) (* C x3) C) ) (- z2 (+ (* C x1) (* C x2) (* C x3) C)))
            ; TODO ellipsoid norm can be done with an upper triangle matrix U by ||Uv|| <= r
                    )
        )
        (X Real (x1 x2))
        (C Real ( (Constant Real) ))
    )
)

; (declare-var x1 Real)
; (declare-var x2 Real)
; (declare-var z1 Real)
; (declare-var z2 Real)

; Define the semantic constraints on the function
; (constraint (inShape 2.372100525863791 0.9678239108338289 0.21114638864503218 3.1077494621276855 (- 0.16957582533359528)) )
; (constraint (inShape 20.547616744645502 0.9678266805486828 0.21114634046254058 0.08310934901237488 (- 0.1517469435930252)) )
; (constraint (inShape 18.006150893559386 0.9678099296179283 0.21114528600009771 3.360142707824707 (- 0.1889626532793045)) )
;(constraint (not (inShape 1 1 0.5 0.5)))
;(constraint (not (inShape 1 1 1.5 1.5)))

; outputs (define-fun inShape ((x1 Real) (x2 Real) (z1 Real) (z2 Real)) Bool (<= (Loo_norm (- z1 (+ (* 0 x1) (* 0 x2) 6)) (- z2 (+ (* 0 x1) (* 1 x2) 0))) 5))
;(constraint (=> (<= (L2_norm (- z1 (+ (* 1 x1) (* 0 x2) 0)) (- z2 (+ (* 1 x1) (* 2 x2) 0))) 2) (inShape x1 x2 z1 z2) ) )

;chiao1
;chiao2
;chiao3


(check-synth)