数组模型中的Z3额外条件（ite子句），当记录类型中有多个数组时

Question

当一条记录包含多个相同类型的命名数组时，我在 z3 中遇到了一些意外行为：

(declare-datatypes () ((Record_lengths (Record_lengths (array (Array Int Int))))))
(declare-datatypes () ((ROI (ROI (array (Array Int Int))))))
(declare-datatypes () ((Record (Record (lengths Record_lengths) (roi ROI)))))
(declare-fun rec () Record)
(assert (= (select (array (lengths rec)) 1) 0))
(get-model)

我预计会有一个解决方案，其中 rec.lengths[1]=0，所有其他都是默认值或随机值。然而lengths 选择器总是有一个额外的ite 子句：

(model 
  (define-fun rec () Record
    (Record (Record_lengths (_ as-array k!1)) (ROI (_ as-array k!0))))
  (define-fun k!0 ((x!0 Int)) Int
    (ite (= x!0 2) 4
      4))
  (define-fun k!1 ((x!0 Int)) Int
    (ite (= x!0 1) 0
    (ite (= x!0 2) 3 ;this is unexpected
      0)))
)

似乎这些额外子句的数量与记录中相同数组类型的数量存在某种关系。 就像在这个例子中一样：Record_lengths 和 ROI 具有相同的类型，如果我在 Record 中添加更多 ROI 类型，那么额外的子句数也会增加。

这是示例的永久链接： https://rise4fun.com/Z3/geoo

Answer 1

SMT 求解器不保证生成的模型在任何意义上都是“最小”的。当然，只要它们生成的模型满足您的所有约束。

话虽如此，您可以使用部分模型的选项并获得“更小”的示例。我在引号中加上了较小的值，因为这里没有最小值的概念；求解器认为模型的一部分以及可以跳过的内容可能会因启发式方法等而异。您可以添加：

(set-option :model.partial true)

到脚本的顶部，看看会产生什么影响。