我想知道的是它们在z3.h中的功能，该功能与seq.mapSMT-LIB 2中的www.example.com相关，解释如下谢谢你的帮助我搜索并看到z3.h但找不到任何功能
d4so4syb1#
实际上，您正在寻找z3_mk_map：https://github.com/Z3Prover/z3/blob/12e45c9d17aa48151b2c20573fb3b527b32fdb54/src/api/api_array.cpp#L166-L189但是，当涉及到使用基于序列的函数时，C API是相当笨拙的，尽管它当然是可行的。我建议使用更高级别的API，而不是使用C来实现这个目的，如果你能避免的话。
1条答案
按热度按时间d4so4syb1#
实际上，您正在寻找z3_mk_map：https://github.com/Z3Prover/z3/blob/12e45c9d17aa48151b2c20573fb3b527b32fdb54/src/api/api_array.cpp#L166-L189
但是，当涉及到使用基于序列的函数时，C API是相当笨拙的，尽管它当然是可行的。我建议使用更高级别的API，而不是使用C来实现这个目的，如果你能避免的话。