如何使用 z3 中的 arg(） 函数

How to use arg() function from z3?

本文关键字：函数 arg 中的 何使用 z3      更新时间：2023-10-16

我最近开始使用带有 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( 没有给我想要的输出。

您必须遍历 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 将是一个好主意，了解所有的复杂性。

相关文章：