Add SMT based encoding

firstpass.smt2

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