使用函数在z3中创建列表(Creating List in z3 using function)

使用函数在z3中创建列表(Creating List in z3 using function)

我试图将这段伪代码转换为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 ) ) ) )

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

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或Viper等研究工具

这里有几点提示：

(insert t l1)表示一个新的列表，通过在t插入t得到。 它不会修改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的值不是静态已知的，那么您很可能需要一个循环不变量或使用固定点来解决未知数量的循环迭代

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

Here are a few pointers:

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