无法突变的Z3数组

Question

我有以下smtlib代码：

(declare-fun res () (Array Int Int))
(declare-fun other () (Array Int Int))
(assert (not (=> (= res other) 
    (forall ((x Int))
                 (< (select res x) 4)))
    ))

(assert (= (select other 0) 1))
(check-sat)
(get-model)

如果我使用z3 4.8.7运行它，则它是SAT，并且我得到这个模型：

(model 
  (define-fun other () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 2 4))
  (define-fun res () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 2 4))
)

这意味着两个数组都被“突变”以填充断言（最后，这使所有子句都失败了）。但我希望其他阵列得到修复。目前，它的行为就像一个变量（例如整数变量），但我希望它是一个常量（例如一个固定的数字，即整数，例如1）。引用语句（声明（=（选择（其他0））1））它仅应在位置0处包含1，并且必须将其固定。有没有办法对此建模？如果另一个数组的行为类似，则上述输入应为UNSAT。

谢谢

Answer 1

如果不希望将其中一个数组视为具有变量解释，则需要使用(define-fun)而不是(declare-fun)进行定义。 clarify-fun声明一个未解释的函数，这意味着Z3可以自由为其分配任何解释。如果您看过，返回的模型将为您提供一些示例，说明如何使用define-fun在smtlib中定义数组。

Answer 2

您说：

它仅应在位置0处包含1，并且必须将其固定。

但是这已经是事实。型号：

 (define-fun other () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 2 4))

您可能会绊倒您。该值是一个常量数组，所有条目都设置为1，但索引2包含值4。

因此，输出已经满足您的约束，并且在索引1处具有值0，这似乎是您要建模的内容。