removing for all constraint

firstpass_learner.sl

 ;; The background theory 
-(set-logic LRA)
+(set-logic NRA)
 
 (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)))
+(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)))
+(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)))
+(define-fun Loo_norm ((x1 Real) (x2 Real)) Real (max  (Abs x1) (Abs x2))) ; squares
 
 (synth-fun inShape ((x1 Real) (x2 Real) (z1 Real) (z2 Real)) Bool
     ;; Declare the non-terminals that would be used in the grammar
@@ -35,6 +35,11 @@
     )
 )
 
+; (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 10 (- 10) 11 (- 11)))
 (constraint (inShape 10 (- 10) 9 (- 9)))
@@ -42,5 +47,7 @@
 (constraint (not (inShape 1 1 0.5 0.5)))
 (constraint (not (inShape 1 1 1.5 1.5)))
 (constraint (not (inShape 9 9 5 5)))
+;(constraint (=> (<= (L2_norm (- z1 (+ (* 1 x1) (* 0 x2) 0)) (- z2 (+ (* 1 x1) (* 2 x2) 0))) 2) (inShape x1 x2 z1 z2) ) )
+
 
 (check-synth)