为什么 Z3 在这个简单的输入上返回"unknown"？

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

这将返回unknown，因为您已经禁用了量词处理机制(例如，您禁用了基于模型的量词实例化模块MBQI)，并且似乎使用您指定的选项，Z3没有启用任何其他机制来确定量化公式，因此它发现它无法确定您的公式并返回unknown。

如果您将其更改为true以启用MBQI，您将收到预期的sat。有多种技术(MBQI，量词消除等)用于确定Z3中的量化公式(请参阅手册中的概述: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