如何将 64 位整数与 boolector 一起使用

Question

我正在尝试使用 boolector 创建模型，但我找不到表示 64 位整数的方法。事实上，数字总是被截断为 32 位。我认为这是因为我使用的是 boolector_int，它有一个 uint32 作为参数（参见 doc）

谁能建议我一种表示这样一个数字的方法？老实说，目前我看不出为什么可以创建 64 位的boolector_bitvec_sort 而boolector_int 只接受uint32。

谢谢

Answer 1

boolector_int 函数用于从实际的int32_t 转换。同样，boolector_unsigned_int 用于从实际的uint32_t 转换。

对于您的用例，请使用以下功能之一：

• boolector_const
• boolector_constd
• boolector_consth

它基本上接受字符串作为参数来放入你的常量。请参阅：https://github.com/Boolector/boolector/blob/ae2a749b858b42c06d436353d8c1857b05021b2e/src/boolector.h#L707-L743

这有点迂回，但本质上你将首先将常量转换为字符串，然后将其传递。 （不同的变体本质上允许二进制、十进制和十六进制表示。）这样您就不必担心该常量的实际宽度，因为这些函数也将目标 sort 作为参数。