从 z3 模型读取 z3 数组的 func interp [英] Read func interp of a z3 array from the z3 model
问题描述
假设我在一个公式中有 2 个数组,我想使用 z3 检查其可满足性.如果 z3 返回 sat,我想读取 z3 模型中的第一个数组并将其打印为键、值对和默认值.后来我想把它转换成地图,并对其做进一步的分析.这是我运行的示例:
Suppose I have 2 arrays in a formula whose satisfiability I want to check using z3. If z3 returns sat, I want to read in the first array in the z3 model and pretty print it as a key, value pair and a default value. Later I want to convert it to a map and do further analysis on it. Here's the example I run:
void find_model_example_arr() {
std::cout << "find_model_example_involving_array\n";
context c;
sort arr_sort = c.array_sort(c.int_sort(), c.int_sort());
expr some_array_1 = c.constant("some_array_1", arr_sort);
expr some_array_2 = c.constant("some_array_2", arr_sort);
solver s(c);
s.add(select(some_array_1, 0) > 0);
s.add(select(some_array_2, 5) < -4);
std::cout << s.check() << "\n";
model m = s.get_model();
std::cout << m << "\n";
expr some_array_1_eval = m.eval(some_array_1);
std::cout << "\nsome_array_1_eval = " << some_array_1_eval << "\n";
func_decl some_array_1_eval_func_decl = some_array_1_eval.decl();
std::cout << "\nThe Z3 expr(fun_decl) for some_array_1_eval is : " << some_array_1_eval_func_decl << "\n";
// ERROR here
func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
// This works well
//func_interp fun_interp = m.get_func_interp(m.get_func_decl(0));
std::cout << "\nThe Z3 expr(fun_interp) for the array is : " << fun_interp << "\n";
unsigned num_entries = fun_interp.num_entries();
for(unsigned i = 0; i < num_entries; i++)
{
z3::func_entry entry = fun_interp.entry(i);
z3::expr k = entry.arg(0);
z3::expr v = entry.value();
std::cout << "\n(key,value): (" << k << "," << v << ")";
}
z3::expr default_value = fun_interp.else_value();
std::cout << "\nDefault value:" << default_value;
}
我得到以下输出:
find_model_example_involving_array
sat
(define-fun some_array_1 () (Array Int Int)
(_ as-array k!0))
(define-fun some_array_2 () (Array Int Int)
(_ as-array k!1))
(define-fun k!0 ((x!1 Int)) Int
(ite (= x!1 0) 1
1))
(define-fun k!1 ((x!1 Int)) Int
(ite (= x!1 5) (- 5)
(- 5)))
some_array_1_eval = (_ as-array k!0)
The Z3 expr(fun_decl) for some_array_1_eval is :
(declare-fun as-array () (Array Int Int))
unexpected error: invalid argument
相反,如果我注释掉第一行并使用第二行,即使用以下代码块:
Instead if I comment out the first line and use the second, ie use the following code block:
// ERROR here
// func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
// This works well
func_interp fun_interp = m.get_func_interp(m.get_func_decl(0));
我得到了我正在寻找的输出:
I get the output I am looking for:
(key,value): (0,1)
Default value:1
问题来了?我如何确定 m.get_func_decl(0) 是对应于 some_array_1 的那个?例如,如果我使用 m.get_func_decl(1),我会得到错误的 (key, value) 对.换句话说,我如何从模型中获取数组的 func_interp(定义为 z3 expr)?
Here's the problem though? How do I figure out that m.get_func_decl(0) is the one corresponding to some_array_1? For instance, if I use m.get_func_decl(1), I get wrong (key, value) pairs. Is other words how do I get a func_interp of an array (defined as a z3 expr) from a model?
推荐答案
数组模型的表示确实有点混乱.
The representation for array models is indeed a bit confusing. The meaning of
(define-fun some_array_1 () (Array Int Int)
(_ as-array k!0))
是数组 some_array_1
的模型是函数 k!0
,它被解释为一个数组(通过调用 as-array
.后者是一个参数函数,它没有参数,因此,要获得 some_array_1 的模型函数的实际定义,我们必须查找 as-array
调用哪个函数. 在给定的示例中,我们可以按如下方式执行此操作,首先通过检查一些断言来确保我们确实拥有预期格式的数组模型:
is that the model for array some_array_1
is the function k!0
which is to be interpreted as an array (signified by the call to as-array
. The latter is a parametric function, which has no arguments, therefore, to get at the actual definition of the model function for some_array_1, we have to look up which function as-array
calls. In the given example, we can do that as follows, first making sure that we actually have an array model in the expected format by checking a few of assertions:
assert(Z3_get_decl_kind(c, some_array_1_eval_func_decl) == Z3_OP_AS_ARRAY);
assert(Z3_is_app(c, some_array_1_eval));
assert(Z3_get_decl_num_parameters(c, some_array_1_eval_func_decl) == 1);
assert(Z3_get_decl_parameter_kind(c, some_array_1_eval_func_decl, 0) ==
Z3_PARAMETER_FUNC_DECL);
func_decl model_fd = func_decl(c,
Z3_get_decl_func_decl_parameter(c, some_array_1_eval_func_decl, 0));
函数声明model_fd
然后保存模型分配的实际函数(k!0
),我们可以通过
The function declaration model_fd
then holds the actual function assigned by the model (k!0
) and we can get the function interpretation via
func_interp fun_interp = m.get_func_interp(model_fd);
这篇关于从 z3 模型读取 z3 数组的 func interp的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!