0

给定表达式 x'=x+1，我希望将 x' 重命名为 y。如何使用z3？

4

1 回答 1

2

有许多 API 函数可让您修改术语并用新子术语替换旧子术语。它们在包含修饰符 Z3_update_term、z3_substitute 和 Z3_substitute_vars 的修饰符部分下进行了描述（还有 Z3_translate 用于在两个上下文之间移植术语）。链接在这里：

http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa7497c70a827db2d61ba98889fe657b5

您还可以直接遍历术语并编写实用程序来修改术语。display_ast 示例显示了递归遍历术语的主要情况：

http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi__ex.html#ga807b5fe0e26acdec09e52a77318208d0
于 2012-09-02T22:31:07.263 回答