expression - 如何在z3中将表达式转换为字符串

Question

有两个 expr_vector A，B，我正在尝试使用比较它们中的元素

if(strcmp(A[i].ToString(),B[i].ToString()) == 1)

并且错误 'class z3::expr' 没有名为 'ToString' 的成员，该成员可在覆盖字符串 ToS​​tring ( ) 上找到。

或者您能告诉我如何比较两个 expr_vector 中的变量吗？比如变量q1分别在向量<expr>A和B中。

Answer 1

您在问题中提供的链接适用于 Z3 C# (.Net) API，您的问题表明您正在使用 C++ API（expr_vector是 Z3 C++ API 的一个类）。

要测试a和b是否相等、wherea和bare z3::expr，我们应该使用eq(a, b). 该eq函数只是 的包装器Z3_is_eq_ast，并定义在z3++.h

friend bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }