使用函数在z3中创建列表

Question

我正在尝试将这段伪代码转换为SMT-LIB语言，但我卡住了。

List function my_fun(int x)
{
    list = nil
    for(i in 1 to x):
        if(some_condition_on_i)
            list.concat(i)
    return list
}

到目前为止我所做的是：

(declare-const l1 (List Int))
(define-fun my_fun ((x Int)) (List Int)
    (forall ((t Int))
        (ite (and (some_condition_on_t) (< t x)) (insert t l1) l1 )
        )
    )
)

我知道这是错的，并且不起作用。你能帮我理解我该怎么办？

Answer 1

SMT-LIB模拟逻辑，其中变量总是不可变的;另一方面，你的代码似乎是必要的，即list和i等变量是可变的。这种至关重要的差异将是编码程序的最大挑战，而对于命令式程序的推理挑战已经引发了诸如Dafny，Boogie或Viper等研究工具

以下是一些指示：

• (insert t l1)代表一个新的列表，通过将t插入l1获得。它不会修改l1（并且没有办法修改l1，因为它是一个逻辑变量）
• 逻辑forall是一个布尔公式（它的计算结果为true或false），它不是一个可以执行的语句（例如，它的副作用）
• 如果x的值是静态已知的（即如果它是5），那么你可以展开循环（这里是伪代码）：

  l0 := Nil
  l1 := ite(condition(1), insert(1, l0), l0)
  l2 := ite(condition(2), insert(2, l1), l1)
  ...
  l4 := ite(condition(4), insert(4, l3), l3)

• 如果x的值不是静态知道的，那么你很可能需要一个循环不变量或者使用修复点来计算未知数量的循环迭代