缺少c++ api的修改方法

missing modification methods on C++ APIs

本文关键字：修改 方法 api c++ 缺少      更新时间：2023-10-16

我想对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没有被取代。我做错了什么吗?

感谢您指出这些功能缺失。c++包装器在C API和它之外增加了便利为这些API函数增加便利性是否合理既然你表明你正在使用它们，

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

以下是一些相关的文章:

  • z3 c++ API &尽管
  • 在Z3中调用一些策略后如何使用枚举常量?
  • 如何读取smtlib2字符串使用z3c++ api?
  • 封装来自z3c API的实体

我相信你的例子有一个打字错误:

  Z3_ast astB = a;

试

  Z3_ast astB = b;

相关文章：