使用函数在 z3 中创建列表 [英] Creating List in z3 using function

问题描述

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

I'm trying to convert this piece of pseudocode to SMT-LIB language, but I got stuck.

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

到目前为止我所做的是:

what I've done so far is this:

(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 )
        )
    )
)

我知道这是错误的，并且不起作用.你能帮我理解我该怎么做吗?

which I know it is wrong, and does not work. can you help me to understand how can I do this?

推荐答案

SMT-LIB 模型逻辑，其中变量总是不可变的；另一方面，您的代码似乎是命令式的，即诸如 list 和 i 之类的变量是可变的.这种关键的差异将是编码程序的最大挑战，并且对命令式程序进行推理的挑战引发了诸如 之类的研究工具Dafny、Boogie 或 毒蛇

SMT-LIB models logic, where variables are always immutable; your code, on the other hand, appears to be imperative, i.e. variables such as list and i are mutable. This crucial difference will be the biggest challenge in encoding your program and the challenge of reasoning about imperative programs has sparked research tools such as Dafny, Boogie, or Viper

这里有一些提示:

• (insert t l1) 表示一个新的列表，通过将t 插入到l1 中获得.它不会不会修改l1(并且没有办法修改l1，因为它是一个逻辑变量)
• 逻辑 forall 是一个布尔公式(它的计算结果为 true 或 false)，它不是一个可以执行的语句(例如它的副作用)

• 如果 x 的值是静态已知的(即如果它是 5)，那么您可以展开循环(此处为伪代码):

• (insert t l1) represents a new list, obtained by inserting t into l1. It will not modify l1 (and there is no way to modify l1 since it is a logical variable)
• A logical forall is a boolean formula (it evaluates to true or false), it is not a statement that you can execute (e.g. for its side effects)

• If the value of x were statically known (i.e. if it were 5), then you could unroll the loop (here in pseudo-code):

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 的值不是静态已知的，那么您很可能需要循环不变性或使用固定点为了解决未知数量的循环迭代

If the value of x isn't statically known then you'll most likely either need a loop invariant or work with fix points in order to account for an unknown number of loop iterations

这篇关于使用函数在 z3 中创建列表的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！