Tests for sheet 6 exercise 3

File contents

;some simple tests for quantifier elimination over the rationals

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

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

(declare-fun y () Real)
(declare-fun z () Real)
(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))))