CODEWITHSUNDEEP
z3smt
william007
william007

Reputation: 18545

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?

Upvotes: 5

Views: 537

Answers (2)

Juan Ospina
Juan Ospina

Reputation: 1347

Possible solution using Redlog of Reduce:

enter image description here

Upvotes: 2

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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

Upvotes: 6

Related Questions