如何使用 z3 中的 arg() 函数? [英] How to use arg() function from z3?

问题描述

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

I have recently started using z3 API with c++ bindings. My task is to obtain the individual element from an expression

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

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

How do I get a individual variables by indexing each position using the function arg(i)?

在给定示例的情况下，arg(1) 应返回变量X".z3 中还有其他函数可以提供我想要的输出吗?

in case of the given example, arg(1) should return the variable 'X'. Is there any other function in z3 that can give me my desired output?

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

This is the code I tried but the output was not a single variable:

#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) 没有给我想要的输出.

I basically need to make an automated system that indexes every position in the expression and check if its an operator or an operand and insert in into a data structure. So I thought ill create a loop and index every position in the expression. But the arg(i) was not giving me my desired output.

推荐答案

您必须遍历 AST 并挑选出节点.Z3 AST 可能相当麻烦，因此在不确切知道您的目标是什么的情况下，很难确定这是否是最佳方法.但是，假设您真的想浏览 AST，您可以这样做:

You have to walk through the AST and pick-out the nodes. Z3 AST can be rather hairy, so without knowing exactly what your goal is, it's hard to opine if this is the best approach. But, assuming you really want to walk through the AST, this is how you'd go about it:

#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);
}

运行时，这个程序打印:

When run, this program prints:

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) 的位置.您可以从这里获取并构建您正在谈论的数据结构.

So, you see exactly where the applications (APP) and arguments (ARGUMENT) are. You can take it from here and construct the data-structure you were talking about.

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

However, beware that a z3 AST can have many different kind of objects: Quantifiers, numbers, bit-vectors, floats. So, studying the actual AST in detail before you start coding would be a good idea to be aware of all the complexities if you want to make this work for an arbitrary z3 expression.

这篇关于如何使用 z3 中的 arg() 函数?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！