从Z3模型阅读Z3阵列的FUNC插值 [英] Read func interp of a z3 array from the z3 model

问题描述

假设我有一个公式我想用Z3检查其可满足2个阵列。如果Z3回报坐着，我想在Z3模型和pretty在第一阵列中读取打印作为重点，对值和默认值。后来我想将其转换为一个地图并在其上做进一步的分析。下面是我运行例如：

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;
}

我得到以下的输出：

I get the following output:

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

相反，如果我注释掉的第一行并使用第二个，即使用以下code座：

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），我拿错（键，值）对。从模型换句话说我如何获得一个数组（定义为Z3表达式）的func_interp？

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?

推荐答案

有关阵列型号重新presentation确实有点混乱。的意义

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 这是间preTED作为数组（通过调用表示为给作为阵列，后者是一个参数函数，它没有参数，因此，要获得在模型的实际定义对于some_array_1功能，我们要回去看看哪个函数作为阵列通话。在给定的例子中，我们可以做到这一点如下，首先确保我们实际上有一个数组模型预期的格式通过检查一些断言：

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插值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！