From 372ccd1fb574c5161208ab863fea2c4b0f31b83c Mon Sep 17 00:00:00 2001
From: Angello Astorga <aastorg2@illinois.edu>
Date: Wed, 15 Dec 2021 21:04:44 -0500
Subject: [PATCH] code to start with a fresh .sl file
---
sygus_learner.py | 5 +++-
template_sygus.sl | 59 +++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 63 insertions(+), 1 deletion(-)
create mode 100644 template_sygus.sl
diff --git a/sygus_learner.py b/sygus_learner.py
index e7aeda0..ec8b3d9 100644
--- a/sygus_learner.py
+++ b/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
diff --git a/template_sygus.sl b/template_sygus.sl
new file mode 100644
index 0000000..747c0b9
--- /dev/null
+++ b/template_sygus.sl
@@ -0,0 +1,59 @@
+;; 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)
--
GitLab