在Z3中从const数组中提取值

Question

我的问题是，在Z3 C/C++ API中，如何从由Z3生成的模型中获取（索引，值）对。

我遇到了与以下问题相同的问题： 从z3模型中读取z3数组的func interp 然而，那个解决方案并不总是适用于我。

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

第一个断言可能会失败，因为函数：

Z3_get_decl_kind(c, some_array_1_eval_func_decl)

返回Z3_OP_CONST_ARRAY，我想知道在这种情况下应该如何提取它。模型是：

(define-fun |choice.pc.1:1| () Bool
  false)
(define-fun pc () (_ BitVec 4)
  #x0)
(define-fun pc_miter_output () Bool
  true)
(define-fun rom () (Array (_ BitVec 4) (_ BitVec 4))
  (_ as-array k!0))
(define-fun |choice.pc.1:2| () Bool
  true)
(define-fun k!0 ((x!0 (_ BitVec 4))) (_ BitVec 4)
  (ite (= x!0 #x0) #x0
    #x0))

我使用它来评估“rom”。如果我打印出结果，那就是：

((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0)

我可以获取它的声明。就是这样

(declare-fun const ((_ BitVec 4)) (Array (_ BitVec 4) (_ BitVec 4)))

如果忽略第一个断言错误并继续执行，第四个断言可能会失败，实际上是Z3_PARAMETER_SORT。

我发现旧版本的Z3库可以使用该答案，但我需要使用更新版本，因为新版本具有to_smt2()函数。

谢谢！

- Hongce Zhang

---

在这种情况下，忽略断言很少是一个好的解决方案 :-) 我没有时间用例子来说明这一点，但你想要的是(as const ...)术语的第一个参数。该术语表示一个常量数组，即该数组对于所有索引具有相同的值。Z3_get_app_arg(ctx, term, 0)应该给你这个值。 - Christoph Wintersteiger

请在您自己的问题下发布答案并接受它 - 这将标记问题为已解决并有助于其他人。 - Malte Schwerhoff

Answer 1

感谢Christoph的提示。我通过以下代码解决了这个问题：

假设

mval = model.eval(...);
mfd = mval.decl();

然后，

while(Z3_get_decl_kind(c.ctx(), mfd) == Z3_OP_STORE) {
    expr addr = mval.arg(1);
    expr data = mval.arg(2);
    // put them into the stack, say __stack__ for later use
    // I omit the code for using them
    mval = mval.arg(0);
    mfd = mval.decl();
    // recursively handle the OP_STORE case, because the first
    // argument can still be an Z3_OP_STORE
}
// now that we peel the Z3_OP_STORE
if(Z3_get_decl_kind(c.ctx(), mfd) == Z3_OP_CONST_ARRAY) {
    expr arg0 = mval.arg(0);
    // we can just use it directly since it is a constant
    std::string sdef(Z3_get_numeral_string(context, arg0));
    // I omit the code for using that value
}
else if( Z3_get_decl_kind(c.ctx(), mfd) == Z3_OP_AS_ARRAY ) {
    // HERE is the original code for handling original case.
    // in the question from the link: 
    // https://dev59.com/m37aa4cB1Zd3GeqPp2kB#22918197
    // 
}

希望这对其他人有所帮助。

- Hongce Zhang