;some simple tests for quantifier elimination over the rationals

(set-option :print-terms-cse false)
(set-logic LRA)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)

;last week's exercises
(simplify (exists ((y Real)) (and (= x (* 2 y)) (< y x))))
(simplify (forall ((y Real)) (or (< 25 (+ x (* 2 y))) (< (+ x (* 2 y)) 25))))
;here you need to call simplify on the result again
(simplify (forall ((x Real)) (exists ((y Real)) (and (> y x) (< (- y) x)))))
(simplify (forall ((x Real)) (= (> x 0) (exists ((y Real)) (and (> x y) (< (- x) y))))))

;some more tests
(simplify (=> (exists ((x Real)) (=> (or (= x (+ 1 2)) (= (* x 3) 6)) (>= (* 4 x) 4))) (forall ((x Real)) (=> (and (= x 5) (not (= x 6))) (<= x 7)))))

(simplify (exists ((x Real)) (=> (= x (+ 1 2)) (>= (* 4 x) 4))))

(simplify (exists ((x Real)) (and (< (+ (* 3 x) 1) 10) (> (- (* 7 x) 6) 7))))
(simplify (exists ((x Real)) (and (> (* 2 x) y) (< (* 3 x) z))))

(simplify (forall ((x Real)) (forall ((y Real)) (=> (> x y) (>= x y)))))
(simplify (forall ((x Real)) (not (> x x))))