小编Tus*_*har的帖子

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

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

  // …