firstpass_learner.sl 5.16 KiB
;; 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) ) )
(constraint (inShape 4.765463957714702 (- 0.9678235924238532) 0.2111463885489226 0.9355837106704712 (- 0.21412937343120575)))
(constraint (inShape 4.765463632180135 (- 0.9678235315764336) 0.21114631398199063 0.8767245411872864 (- 0.20872043073177338)))
(constraint (inShape 4.765469434861616 (- 0.9678222760374098) 0.21114633781371142 0.8548175096511841 (- 0.20760071277618408)))
(constraint (inShape 4.765472132991584 (- 0.967821690209135) 0.2111463135604636 0.8481259346008301 (- 0.20709337294101715)))
(constraint (inShape 26.014448722969494 (- 0.9678236080554914) 0.21114638862599663 0.9063019752502441 (- 0.21251192688941956)))
(constraint (inShape 26.014445186473395 (- 0.9678243278961034) 0.21114665030099153 0.849083423614502 (- 0.20872122049331665)))
(constraint (inShape 26.01445259548303 (- 0.9678226318697245) 0.2111464041592506 0.8819234371185303 (- 0.2109939455986023)))
(constraint (inShape 26.014455372438157 (- 0.967822032009428) 0.21114628958749526 0.8592063784599304 (- 0.20877516269683838)))
(constraint (inShape 26.014460524474426 (- 0.9678209148025161) 0.21114630912352733 0.2559255361557007 (- 0.17408597469329834)))
(constraint (inShape 20.07743429421359 (- 0.9678235953796133) 0.21114638864717244 0.32362231612205505 (- 0.17972034215927124)))
(constraint (inShape 20.077401903788825 (- 0.9678294397256906) 0.21114585965862093 (- 0.6266307830810547) 0.04582478478550911))
(constraint (inShape 20.07744007331555 (- 0.9678222060049109) 0.21114636311895862 (- 0.6973455548286438) 0.04908551648259163))
(constraint (inShape 20.077442852607035 (- 0.9678216080262558) 0.21114631408943035 (- 0.6066773533821106) 0.04362167418003082))
(constraint (inShape 5.993772873635214 (- 0.9678235959898132) 0.2111463887360923 0.9497198462486267 (- 0.21268075704574585)))
(constraint (inShape 5.993775929900048 (- 0.9678227989056012) 0.21114617156117935 0.9282993674278259 (- 0.20913195610046387)))
(constraint (inShape 5.993781491794785 (- 0.9678215943141169) 0.21114627376922074 0.9325944781303406 (- 0.20973370969295502)))
(constraint (inShape 5.993784071107384 (- 0.9678210348414424) 0.21114634014029712 0.8477240204811096 (- 0.20398835837841034)))(constraint (inShape 2.9876647902045153 (- 0.9678235940334616) 0.21114638864409163 0.8357511162757874 (- 0.20139506459236145)))
(constraint (inShape 2.987666363074242 (- 0.9678231185708412) 0.21114621408801454 0.8440750241279602 (- 0.20274119079113007)))
(constraint (inShape 2.987672058705376 (- 0.967821885735006) 0.2111463087908345 0.843758761882782 (- 0.20223206281661987)))
(constraint (not (inShape (- 0.07083899923294591) (- 1.995804969797873) (- 1.0402636607228553) 0.0 0.0)))
(constraint (not (inShape 0.05005137750787882 (- 1.985812931697809) (- 1.326396471233834) 0.0 (- 1.326396471233834))))
(constraint (not (inShape (- 0.13999904590704734) 0.0 0.0 0.0 0.0)))
(constraint (not (inShape (- 0.035084224611038786) (- 1.001789119936619) 1.313916457014109 0.0 0.0)))
(check-synth)