假设我在公式中有 2 个数组，我想使用 z3 检查其可满足性。如果 z3 返回 sat，我想读取 z3 模型中的第一个数组，并将其打印为键、值对和默认值。稍后我想将其转换为 map 并对其进行进一步分析。这是我运行的示例:

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

相反，如果我注释掉第一行并使用第二行，即使用以下代码块:

// 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)); 

我得到了我正在寻找的输出:

(key,value): (0,1)
Default value:1

问题来了？我如何确定 m.get_func_decl(0) 是对应于 some_array_1 的那个？例如，如果我使用 m.get_func_decl(1)，我会得到错误的(键、值)对。换句话说，如何从模型中获取数组的 func_interp(定义为 z3 expr)？

最佳答案

数组模型的表示确实有点困惑。的含义

(define-fun some_array_1 () (Array Int Int)   
  (_ as-array k!0)) 

是数组 some_array_1 的模型是函数 k!0，它被解释为一个数组(通过调用 as-array 表示。后者是一个参数函数，没有参数，因此，要获得 some_array_1 模型函数的实际定义，我们必须查找 as-array 调用的函数. 在给定的示例中，我们可以按如下方式执行此操作，首先通过检查一些断言来确保我们确实拥有预期格式的数组模型:

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) 我们可以通过以下方式获得函数解释

  func_interp fun_interp = m.get_func_interp(model_fd);

关于c++ - 从 z3 模型读取 z3 数组的 func interp，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22885457/