如何从 Lambda 表达式中获取值? [英] How get a a value from a Lambda expression?

问题描述

我正在 python 中试验 z3.我有以下模型:

(set-option :produce-models true)(设置逻辑 QF_AUFBV )(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )(assert (and (= false (= (_ bv77 32)) (concat (select a (_ bv3 32) ) (concat (select a (_ bv2 32) ) (concat (select a (_ bv1 32) ) (select a(_ bv0 32) ) ) ) ) ) (= false (= (_ bv12 32) (concat (select another (_ bv3 32) ) (concat (select another (_ bv2 32) ) (concat (select another (_bv1 32) ) (选择另一个 (_ bv0 32) ) ) ) ) ) ) )

我可以加载它并检查它是否已坐.在这一点上，我如何获得 a 和 another 的示例值?

导入z3s = z3.Solver()s.from_file("first.smt")"""秒[和(假==(77 == Concat(a[3], Concat(a[2], Concat(a[1], a[0])))),错误==(12 ==Concat(另一个[3],Concat(另一个[2],连接(另一个[1]，另一个[0])))))]"""s.check()"""坐"""m = s.model()米[a = Lambda(k!0, 1)，另一个 = Lambda(k!0, 1)]

谢谢

解决方案

Z3 默认为数组生成 Lambda 抽象；这很有用，但很难看到模型中发生了什么.我建议关闭它，在你的 python 程序中加入以下行:

z3.set_param('model_compress', False)

您应该在 import z3 之后立即执行此操作.

有了这个，如果你在你的程序中打印模型，你会得到:

<预><代码>>>>米[a = [3 ->1, 否则 ->1],另一个 = [1 ->1, 否则 ->1],k!0 = [3 ->1, 否则 ->1],k!1 = [1 ->1, 否则 ->1]]]

这应该更具可读性.(本质上是说 a 和 another 都是将所有内容都映射到 1 的数组；虽然有点复杂.)

I'm experimenting with z3 in python. I have the following model:

(set-option :produce-models true)
(set-logic QF_AUFBV )
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun another () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and  (=  false (=  (_ bv77 32) (concat  (select  a (_ bv3 32) ) (concat  (select  a (_ bv2 32) ) (concat  (select  a (_ bv1 32) ) (select  a (_ bv0 32) ) ) ) ) ) ) (=  false (=  (_ bv12 32) (concat  (select  another (_ bv3 32) ) (concat  (select  another (_ bv2 32) ) (concat  (select  another (_ bv1 32) ) (select  another (_ bv0 32) ) ) ) ) ) ) ) )

I can load it and check that is sat. At this point how can I get an example value for a and another?

import z3
s = z3.Solver()
s.from_file("first.smt")
"""
s
[And(False ==
     (77 == Concat(a[3], Concat(a[2], Concat(a[1], a[0])))),
     False ==
     (12 ==
      Concat(another[3],
             Concat(another[2],
                    Concat(another[1], another[0])))))]
"""
s.check()
"""
sat
"""
m = s.model()
m
[a = Lambda(k!0, 1), another = Lambda(k!0, 1)] 

Thanks

解决方案

Z3 produces Lambda abstractions for arrays by default; which are useful but hard to see what's going on in a model. I'd recommend turning that off, by putting the following line in your python program:

z3.set_param('model_compress', False)

You should do this right after you import z3.

With this, if you print the model in your program, you get:

>>> m
[a = [3 -> 1, else -> 1],
 another = [1 -> 1, else -> 1],
 k!0 = [3 -> 1, else -> 1],
 k!1 = [1 -> 1, else -> 1]]

which should be more readable. (It's essentially saying both a and another are arrays that map everything to 1; though a bit convoluted.)

这篇关于如何从 Lambda 表达式中获取值?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！