code to start with a fresh .sl file

sygus_learner.py

@@ -5,10 +5,13 @@ from z3 import *
 
 from learner_base import LearnerBase
 import re
+import shutil
 
 class SygusLearner(LearnerBase):
     def __init__(self, state_dim, perc_dim, timeout=10000):
-         self.file = 'shapes_split.sl'
+        self.file = 'shapes_split.sl'
+        self.template_file = 'template_sygus.sl'
+        shutil.copyfile(self.template_file, self.file )
 
     def set_grammar(self, grammar) -> None:
         raise NotImplementedError

template_sygus.sl

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