0

我正在使用 Z3-3.2 的 c-api（在 linux 上）来解决 QF_AUFBV 问题。

如果公式可以满足，我想从模型中读出自由数组变量的值。

我尝试了以下代码的一些内容，我想知道如何做到这一点的总体思路是否正确：

void evaluate(Z3_context context, Z3_model model, Z3_ast array)
{
  Z3_ast value;
  Z3_bool success = Z3_eval(context, model, array, &value);
  if (success) {
    unsigned num_entries;
    if (Z3_is_array_value(context, model, value, &num_entries)) {
      Z3_ast indices[num_entries];
      Z3_ast values[num_entries];
      Z3_ast def;
      Z3_get_array_value(context, model, array, num_entries, indices, values, &def);

      // do something with indices, values, and def
    }
  }
}

输入 Z3_ast 数组绝对是一个自由数组表达式。Z3_eval 返回 true，因此我们似乎已经成功评估了表达式，但随后 Z3_is_array_value 返回 false。我本来希望数组表达式上成功的 Z3_eval 的结果是数组值，那么为什么不是这样呢？

顺便说一句：我们通过遍历所有 model_func_decls 并尝试通过比较它们的 get_symbol_string 来尝试为该数组找到正确的信息，从而获得了所需的信息。所以这些信息似乎在 Z3 的某个地方可用，但这算不上一个好的解决方案。

感谢您对此的任何帮助。

最好的问候，弗洛里安

4

1 回答 1

0

评估器比用于访问数组值的 API 更强大。函数 is_array_value 仅在表示的数组的形式为 (store (store (store (... (const v) ...) ..)..)) 或形式为 as-array[f] 时才成功，其中f 是有限一元函数。

is_array_value 和 get_array_value 函数可以使用现有的 API 实现，并且为了方便而公开（如您所述，除了我们可以避免使用字符串比较，而是在作为枚举排序的函数声明上使用比较）。所以听起来我们可以在你的情况下支持更多，我很好奇模型值的样子。您能否提供有关未通过示例的其他信息？（打印出来？）

谢谢

于 2012-02-09T22:17:59.817 回答