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

的绑定