如何隱藏變量與Z3

t1<x and x<t2

是有可能隱藏變量x所以Z3是 t1<t2 ？

2012-07-24 william007

你可以使用量詞消去來做到這一點。這裏有一個例子：

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

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

你可以試試這個例子在網上：http://rise4fun.com/Z3/kp0X

2012-07-24 11:27:12

謝謝，但爲什麼結果是T1-T2 < = -2？而不是t1-t2 <0？ – william007 2012-07-26 07:44:14

因爲't1'，'t2'和'x'是整數。對於整數，如果'a 2012-07-26 14:42:54

這個答案似乎已經過時了，因爲它產生了「不受支持」的結果（同樣在rise4fun上） – DCTLib 2016-11-28 20:26:29

可能的解決方案使用的Redlog減少：

enter image description here

2013-07-28 20:31:05

回答