From 4acae8f4b5e4b180f44f017184e08badbc79a467 Mon Sep 17 00:00:00 2001
From: "Hsieh, Chiao" <chsieh16@illinois.edu>
Date: Mon, 29 Nov 2021 12:02:12 -0600
Subject: [PATCH] Add SMT based encoding

---
 firstpass.smt2 | 57 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 57 insertions(+)
 create mode 100644 firstpass.smt2

diff --git a/firstpass.smt2 b/firstpass.smt2
new file mode 100644
index 0000000..f3611e6
--- /dev/null
+++ b/firstpass.smt2
@@ -0,0 +1,57 @@
+; (set-logic NRA)
+(set-logic LRA)
+
+; Variable declarations
+(declare-fun a00 () Real)
+(declare-fun a01 () Real)
+(declare-fun b0 () Real)
+
+(declare-fun a10 () Real)
+(declare-fun a11 () Real)
+(declare-fun b1 () Real)
+
+(declare-fun radius () Real)
+
+; Constraints
+(assert (>= radius 0.0))
+
+; (define-fun norm ((x Real) (y Real)) Real (+ (* x x) (* y y)))
+(define-fun Abs ((x Real)) Real (ite (>= x 0) x (- x)))
+(define-fun norm ((x Real) (y Real)) Real (+ (Abs x) (Abs y)))
+
+(define-fun err ((x Real) (y Real)) Real (Abs x))
+
+(define-fun transitionX ((x Real) (xP Real)) Real 
+     (ite (> xP 0) (- x 1) (ite (= xP 0) x (+ x 1)))
+)
+
+(define-fun transitionY ((y Real) (yP Real)) Real 
+     (ite (> yP 0) (- y 1) (ite (= yP 0) y (+ y 1)))
+) 
+
+(define-fun inCircle ((x Real) (y Real) (xP Real) (yP Real)) Bool
+     (<=
+          (norm
+               (+ (- xP) (* 1 x) (* 0 y) b0)
+               (+ (- yP) (* 0 x) (* 1 y) b1)
+          )
+          radius
+     )
+) 
+
+(assert (inCircle 1 1 1.2 0.8))
+(assert (inCircle 10 -10 9 10.8))
+
+(assert (forall ((xx Real) (yy Real) (xxP Real) (yyP Real))
+     (=>
+          (and (inCircle xx yy xxP yyP) (>= xx 5) (>= yy 5))
+          (<= (err (transitionX xx xxP) (transitionY yy yyP)) (err xx yy) )
+     )
+))
+
+(apply (then qe nnf) :print false :print-benchmark true)
+;(apply (! qe :qe-nonlinear true))
+
+; Solve
+;(check-sat)
+;(get-model)
-- 
GitLab