1. 首页
  2. 问答
  3. 如何隐藏变量与Z3

如何隐藏变量与Z3

2012-07-24 55 views

回答

6

你可以使用量词消去来做到这一点。这里有一个例子：

(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

+0

谢谢，但为什么结果是T1-T2 < = -2？而不是t1-t2 <0？ – william007 2012-07-26 07:44:14

+1

因为't1'，'t2'和'x'是整数。对于整数，如果'a 2012-07-26 14:42:54

+1

这个答案似乎已经过时了，因为它产生了“不受支持”的结果（同样在rise4fun上） – DCTLib 2016-11-28 20:26:29

1

可能的解决方案使用的Redlog减少：

enter image description here

来源

2013-07-28 20:31:05

相关问题

 相关问题