在C ++中获取Z3中位向量的数值

Question

我尝试使用以下API求解后从位向量中获取数值

u64 value; 
Z3_get_numeral_uint64(myContext(),myBitVector,&value);

但是value中的结果为十进制形式，如何以十六进制形式返回它？

Answer 1

这确实与z3无关。十六进制（或任何其他基数）表示形式就是您将字符以字符串形式记下来的方式。表示为一系列位的基础位模式总是这样：一堆0和1。

要进行后处理，您最有可能的意思是将数字的“十六进制”表示形式作为字符串，并对其进行处理。在C语言中，您可以使用sprintf将您的数字以字符串的形式显示在各个基数中，然后对它们进行处理。类似于：

#include <stdint.h>
#include <stdio.h>
#include <inttypes.h>
#include <stdint.h>
#include <string.h>

int main(void) {
  uint64_t i = 253;

  char buf[100];
  sprintf(buf, "%"PRIx64, i);

  // Now post-process in any way you want.
  // I'll just add -- HELLO to the end.
  strcat(buf, " -- HELLO");

  printf("%s\n", buf);

  return 0;
}

当我运行它时，我得到：

$ make a
c++     a.cpp   -o a
$ ./a
fd -- HELLO

这是因为用十六进制写的253是fd，然后我在其中添加了其他字符串，即对其进行了后处理。

再次，重要的是要强调，这与z3无关，而不同基数的数字只是用ASCII表示它们的方式。在内部，它只是一堆比特，谈论它是十六进制，八进制，十进制还是任何其他基数都没有任何意义。