如何使用 z3 中的 arg() 函数？

Question

我最近开始使用带有 c++ 绑定的 z3 API。我的任务是获取 表达式中的单个元素

示例：(x || !z) && (y || !z) && (!x || !y || z)

如何通过使用函数 arg(i) 对每个位置进行索引来获取单个变量？

在给定示例的情况下，arg(1) 应返回变量“X”。 z3 中是否还有其他功能可以提供我想要的输出？

这是我尝试过的代码，但输出不是单个变量：

#include<iostream> 
#include<string>
#include "z3++.h"
using namespace z3;

int main()
{
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr z = c.bool_const("z");
    expr prove = (x || !z) && (y || !z) && (!x || !y || z);
    solver s(c);
    expr argument = prove.arg(1);
    std::cout<<argument;  
}

输出：

(or (not x) (not y) z)(base)

我基本上需要创建一个自动化系统来索引表达式中的每个位置，并检查它是运算符还是操作数，然后插入到数据结构中。所以我想我会创建一个循环并索引表达式中的每个位置。但是 arg(i) 并没有给我我想要的输出。

Answer 1

您必须遍历 AST 并挑选出节点。 Z3 AST 可能相当棘手，因此在不确切知道您的目标是什么的情况下，很难判断这是否是最佳方法。但是，假设您真的想通过 AST，您可以这样做：

#include<iostream>
#include<string>
#include "z3++.h"
using namespace z3;
using namespace std;

void walk(int tab, expr e)
{
    string blanks(tab, ' ');

    if(e.is_const())
    {
        cout << blanks << "ARGUMENT: " << e << endl;
    }
    else
    {
        cout << blanks << "APP: " << e.decl().name() << endl;
        for(int i = 0; i < e.num_args(); i++)
        {
            walk(tab + 5, e.arg(i));
        }
    }
}

int main()
{
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr z = c.bool_const("z");
    expr e = (x || !z) && (y || !z) && (!x || !y || z);

    walk(0, e);
}

运行时，此程序会打印：

APP: and
     APP: and
          APP: or
               ARGUMENT: x
               APP: not
                    ARGUMENT: z
          APP: or
               ARGUMENT: y
               APP: not
                    ARGUMENT: z
     APP: or
          APP: or
               APP: not
                    ARGUMENT: x
               APP: not
                    ARGUMENT: y
          ARGUMENT: z

因此，您可以准确地看到应用程序 (APP) 和参数 (ARGUMENT) 的位置。您可以从这里获取并构建您所说的数据结构。

但是，请注意 z3 AST 可以有许多不同类型的对象：量词、数字、位向量、浮点数。因此，如果您想让它适用于任意 z3 表达式，那么在开始编码之前详细研究实际的 AST 将是一个好主意，了解所有复杂性。