评估数组表达式
问题描述:
我正在使用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的某个地方找到,但这很难算是一个很好的解决方案。
感谢您的任何帮助。
此致 弗洛里安
答
评价者比用于访问数组值的API功能更强大的一点。 函数is_array_value只有在表示数组的形式为 (store(store(store(...(const v)...)..))) 或as-array [f ],其中f是一个有限一元函数。
的is_array_value和get_array_value功能,可以利用现有的API 实现,并且暴露方便 (象你所说的,除了我们能避免使用字符串比较,而使用比较上 函数声明是枚举排序)。 所以这听起来像我们可以在你的情况下支持更多,我很好奇模型的外观。您能否提供有关未通过示例的其他信息? (打印?)
谢谢