为什么Z3返回“未知"?在这个简单的输入? [英] Why does Z3 return "unknown" on this simple input?

问题描述

这是输入:

(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.

Note that Z3 does not timeout. It returns unknown almost instantaneously.

推荐答案

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

This returns unknown because you've disabled the quantifier handling mechanism (e.g., you disabled the model based quantifier instantiation module, MBQI), and it appears that with the options you've specified, Z3 does not have any other mechanisms enabled for deciding quantified formulas, so it figures out that it cannot decide your formula and returns unknown.

如果您将其更改为 true 以启用 MBQI，您将按预期收到 sat.有多种技术(MBQI、量词消除等)可用于确定 Z3 中的量化公式(请参阅此处的手册了解概述:http://rise4fun.com/z3/tutorialcontent/guide#h28 )，例如，对于您的示例，您还可以使用宏查找器模块(rise4fun 链接: http://rise4fun.com/Z3/NuQg ):

If you change that to true to enable MBQI, you will receive sat as expected. There are a variety of techniques (MBQI, quantifier elimination, etc.) for deciding quantified formulas in Z3 (see in the manual here for an overview: http://rise4fun.com/z3/tutorialcontent/guide#h28 ), e.g., for your example, you can also get sat as expected using the macro finder module (rise4fun link: 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

这篇关于为什么Z3返回“未知"?在这个简单的输入?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！