从 Z3 中的 const 数组中提取值答案

【问题标题】：Extract value from const array in Z3从 Z3 中的 const 数组中提取值
【发布时间】：2016-12-01 05:53:40
【问题描述】：

我的问题是，在 Z3 C/C++ API 中，如何从 Z3 生成的模型中获取 (index,value) 对。

我遇到了同样的问题， Read func interp of a z3 array from the z3 model

但是，该解决方案并不总是适合我。

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() 函数。

谢谢！

【问题讨论】：

在这种情况下，忽略断言很少是一个好的解决方案 :-) 我没有时间在示例中说明这一点，但您想要的是 (as const ...) 术语的第一个参数.该术语表示一个常量数组，即该数组对于所有索引具有相同的值。 Z3_get_app_arg(ctx, term, 0) 应该给你价值。
请发布您自己问题的答案并接受它 - 这会将问题标记为已解决并可能帮助其他人。

标签： arrays z3

【解决方案1】：

感谢克里斯托夫的提示。我通过以下代码解决了这个问题：

假设

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: 
    // http://stackoverflow.com/questions/22885457/read-func-interp-of-a-z3-array-from-the-z3-model/22918197#22918197?newreg=1439fbc25b8d471981bc56ebab6a8bec
    // 
}

希望对其他人有所帮助。

【讨论】：