How to hide variable with Z3

问题:

Say I have

t1<x and x<t2

is it possible to hide variable x so that t1<t2 in Z3?

回答1:

You can use quantifier elimination for doing that. Here is an example:

(declare-const t1 Int)
(declare-const t2 Int)

(elim-quantifiers (exists ((x Int)) (and (< t1 x) (< x t2))))

You can try this example online at: http://rise4fun.com/Z3/kp0X

回答2:

Possible solution using Redlog of Reduce: