如何使用 cpp 将 z3 表达式转换为字符串

How to convert and z3 expression to string using cpp?

本文关键字：转换 字符串 表达式 z3 何使用 cpp      更新时间：2023-10-16

我正在尝试创建一个映射到我的表达式变量和具有随机整数值的表达式常量。
这是表达式：((x || !z) && (y || !z))其中 x y 和 z 是bool_const表达式。

我创建了一个递归函数，它能够遍历表达式中的每个元素。但是在映射函数中，我必须给出一个整数和一个字符串作为输入。

map<int,string> symbols; 
void walk(expr e)
{     
    if(e.is_const())
    {   
        std::cout <<"ARGUMENT: " << e<< endl;
        int ran_num = (rand() % 10) + 1;
        symbols.insert(pair<int,string>(ran_num,e.to_string)); 
    }
    else
    {
        cout <<"APP: " << e.decl().name() << endl;
        for(int i = 0; i < e.num_args(); i++)
        {    int ran_num = (rand() % 10) + 1;
             symbols.insert(pair<int,string>(ran_num,e.decl().name())); 
             walk(e.arg(i));
        }
    }
}

这里出现问题 

symbols.insert(pair<int,string>(ran_num,e.to_string)

其中e.to_string无法解释为字符串

和 

symbols.insert(pair<int,string>(ran_num,e.decl().name()))

也无法将e.decl().name()部分解释为 STRING。

如何将它们转换为字符串以满足我的映射函数？

正如编译器告诉你的，name 不是一个string，它是一个symbol，定义在这里：https://z3prover.github.io/api/html/classz3_1_1symbol.html

如果你想把它变成一个字符串，它确实提供了一个str的方法;所以你应该说e.decl().name().str()。

但在进入细节之前，您应该首先查看表示 Z3 表达式的类层次结构。从这里开始： https://z3prover.github.io/api/html/classz3_1_1expr.html

相关文章：