0

我想对 z3::expr 对象进行一些转换。如何使用Z3_substitute_vars,Z3_translate和Z3_substitute_C++ API？它们是用 C# 实现的，但我在 C++ 中找不到它们。很奇怪，它们没有被执行。

我尝试使用 C api 但没有任何结果，这里有一个例子：

void substitute(){
z3::context c;
z3::expr a = c.int_const("a");
Z3_ast astA = a;
z3::expr plus = 2*a;
errs() << Z3_ast_to_string(c,plus);
z3::expr b = c.int_const("b");
Z3_ast astB = a;
z3::expr subs(c,Z3_substitute(c,plus,1,&astA,&astB));
errs() << Z3_ast_to_string(c,subs);
}

但a不会被替代。难道我做错了什么？

4

2 回答 2

2

感谢您指出这些功能不存在。C++ 包装器增加了 C API 之外的便利，并且为这些 API 函数添加便利也是合理的，因为您表明您正在使用它们。

C++ 包装器仍然可以与基本的 C API 一起使用。因此，您可以在使用 C++ API 时调用函数，例如 Z3_translate 和 Z3_substitute。许多其他 API 函数也没有出现在 C++ 包装器中，但是现有函数的包装方式应该很好地说明了如何调用剩余的函数。

以下是一些相关的帖子：

于 2013-04-17T15:47:18.770 回答
1

我相信你的例子有一个错字：

  Z3_ast astB = a;

尝试

  Z3_ast astB = b;
于 2013-04-18T17:10:35.940 回答