我想知道列表的z3理论是否可判定？看起来我们只能证明事实是不完整但不能使用理论，所以我很好奇它是否真的可以判断 . 谢谢你的帮助 .
在Z3中，当我们说理论是可判定的时，我们通常会谈论量词免费问题 . 在Z3中实现的列表理论是可判定的 . 但是，只要我们使用量词和未解释的函数（如问题cross product in z3），问题就变得不可判定 . Z3可以决定一些片段，但cross product in z3中描述的问题不在Z3支持的任何片段中 . 实际上，Z3将无法为类似于此问题的任何问题构建模型 . 因此，它将永远运行，试图 Build 一个模型，或将放弃返回 unknown . 结果 unknown 可能仍然有用 . 在某些情况下，Z3可能会产生"candidate model" . 也就是说，一种解释不能满足你的问题中的所有通用公式，但满足所有量词免费公式，以及通用公式的许多实例 . 为此，我们必须禁用模块MBQI . 启用MBQI后，Z3将继续尝试查找满足所有量词的解释 . 以下是我们为您举办的示例：
unknown
http://rise4fun.com/Z3/kGtk
诀窍是我在脚本开头包含的以下两个命令：
(set-option :auto-config false) (set-option :mbqi false)
我使用 get-value 命令来显示Z3产生的解释满足 (assert (= (first (head l)) a)) . 另一方面， append 的解释并不真正满足本例中的通用公式 .
get-value
(assert (= (first (head l)) a))
append
1 回答
在Z3中，当我们说理论是可判定的时，我们通常会谈论量词免费问题 . 在Z3中实现的列表理论是可判定的 . 但是，只要我们使用量词和未解释的函数（如问题cross product in z3），问题就变得不可判定 . Z3可以决定一些片段，但cross product in z3中描述的问题不在Z3支持的任何片段中 . 实际上，Z3将无法为类似于此问题的任何问题构建模型 . 因此，它将永远运行，试图 Build 一个模型，或将放弃返回
unknown. 结果unknown可能仍然有用 . 在某些情况下，Z3可能会产生"candidate model" . 也就是说，一种解释不能满足你的问题中的所有通用公式，但满足所有量词免费公式，以及通用公式的许多实例 . 为此，我们必须禁用模块MBQI . 启用MBQI后，Z3将继续尝试查找满足所有量词的解释 . 以下是我们为您举办的示例：http://rise4fun.com/Z3/kGtk
诀窍是我在脚本开头包含的以下两个命令：
我使用
get-value命令来显示Z3产生的解释满足(assert (= (first (head l)) a)). 另一方面，append的解释并不真正满足本例中的通用公式 .