Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
; (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