z3 - Z3 中的位向量表达扩展

Question

我有一个 32 位的位向量表达式。不知何故，我想对此表达式进行有符号或无符号扩展为 64 位位向量。有我可以使用的 API 吗？

Answer 1

对于符号扩展:

Z3_ast Z3_API Z3_mk_sign_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1); https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h#L2826

对于未签名的扩展:

Z3_ast Z3_API Z3_mk_zero_ext(__in Z3_context c, __in unsigned i, __in Z3_ast t1); https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h#L2838

这些函数也可用于 Python、C#、Java 的绑定(bind)