为什么Z3在这个简单的输入上返回“未知”？

Question

这里是输入：

(set-option :auto-config false) 
(set-option :mbqi false) 
(declare-sort T6) 
(declare-sort T7) 
(declare-fun set23 (T7 T7) Bool) 
(assert (forall ((bv1 T7) (bv0 T7)) 
    (= (set23 bv0 bv1) (= bv0 bv1)))) 
(check-sat) 

注意Z3不会超时。它几乎是瞬间返回unknown。

Answer 1

由于您已禁用量词处理机制（例如，您禁用了基于模型的量词实例化模块MBQI），因此返回未知，并且您看到使用您指定的选项，Z3没有任何其他机制可用于确定量化公式，因此它会发现它无法确定您的公式并返回未知数。

如果您将其更改为true以启用MBQI，您将收到按预期方式发送的信息。用于决定Z3中量化公式的各种技术（MBQI，量化器消除等）（参见本手册中的概述：http://rise4fun.com/z3/tutorialcontent/guide#h28），例如，对于您的示例，您也可以使用宏查找器模块（rise4fun链接：http://rise4fun.com/Z3/NuQg）：

(set-option :auto-config false) 
(set-option :mbqi false) 
(set-option :macro-finder true) 

(declare-sort T6) 
(declare-sort T7) 
(declare-fun set23 (T7 T7) Bool) 
(assert (forall ((bv1 T7) (bv0 T7)) 
    (= (set23 bv0 bv1) (= bv0 bv1)))) 
(check-sat) ; sat