带有量词和数组的z3以及Seahorn的相应C代码

编程问答 2022-08-13

问题描述

下面的程序在z3上运行时返回unsat。

(assert ( forall ( (y (Array Int Int)) ) 
   (= (select y 1) 0) 
))
(check-sat)

我不明白，“ forall”行实际上是什么意思；对于所有数组-Int y [Int]，是否意味着y [1] == 0？如果是，那么是SAT，否则是UNSAT？当我运行上面的代码时，为什么z3返回unsat？

这是我为Seahorn编写的C代码，对应于上述smt2文件。

#include "seahorn/seahorn.h"
extern int nd();

int main(void){

int n = nd();

assume(n>0);

int y[n]; 

for(int i = 0; i < n; i++)
{
    sassert(y[1]=0);        
}

}

我使用Seahorn将C代码转换为smt2文件，然后使用CHC Comp 2020中的format.py对其进行格式化，然后在格式化文件上运行z3，结果为-unsat。

尽管，两个文件的答案相同，但我认为这不是正确的代码。原始的smt2文件说“ Forall array y”，而我的C代码说“对数组y中的所有元素”。如何为该问题编写正确的C代码？

[请注意：我参考了z3的教程，但仍然不清楚]

解决方法

此断言的含义：

(assert ( forall ( (y (Array Int Int)) ) 
   (= (select y 1) 0) 
))

is：对于所有用整数索引并包含整数的数组y，位置1上的元素始终为0。

很显然，这是无法满足的。在许多数组中，1位置的元素不为0，因此您的量化断言失败，并且您得到unsat作为答案。

请注意，除非它声明了一些琐碎的事情，否则任何关于数组的通用量化公理都注定是不满足的：对于所有这样的数组，您可以写出什么属性正确？没有很多。

很难猜到您要做什么，但是总的来说您想说的是我有一个数组，而且我知道它的第一个元素是0。 ，使用存在性。假定在SMTLib查询的顶级声明的任何变量都是存在的。像这样：

(declare-fun A () (Array Int Int))

; assert first element of `A` is `0`
(assert (= (select A 1) 0))

; .. now add other constraints,etc.

这种方法实质上是告诉z3考虑所有数组A，使它们在第1个位置具有0；并且是通常涉及的软件验证任务的典型代表。 （该约束来自程序的“初始化”部分。）

arraysarraysarraysquantifiersseahornsmtz3