How to hide a variable with Z3

Question

Say I have

t1<x and x<t2

can I hide the variable x so that t1<t2 in Z3?

+5

william007 Jul 24 '12 at 6:35

2 answers

Possible solution using Redlog of Reduce:

+1

Juan ospina Jul 28 '13 at 20:31

Leonardo de moura · Accepted Answer · 2012-07-24T11:27:12+0000

You can use a quantifier exception for this. 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