评估数组表达式

我正在使用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的某个地方找到，但这很难算是一个很好的解决方案。

感谢您的任何帮助。

此致弗洛里安

来源

2012-02-09 user1199435

评价者比用于访问数组值的API功能更强大的一点。函数is_array_value只有在表示数组的形式为（store（store（store（...（const v）...）..）））或as-array [f ]，其中f是一个有限一元函数。

的is_array_value和get_array_value功能，可以利用现有的API 实现，并且暴露方便（象你所说的，除了我们能避免使用字符串比较，而使用比较上函数声明是枚举排序）。所以这听起来像我们可以在你的情况下支持更多，我很好奇模型的外观。您能否提供有关未通过示例的其他信息？（打印？）

谢谢

来源

2012-02-09 22:17:59

评估数组表达式

回答

相关问题