Создать постоянный битвектор

Question

Создать постоянный битвектор

Я очень новичок в Z3 и пытаюсь использовать его bitvector C ++ API. Насколько я понял, метод bv_val (int n, unsigned sz) в контексте класса нацелен на создание битового вектора размера sz со значением n.
Но почему значение n ограничено типом int? Что произойдет, если я создам битовый вектор размером 10 со значением, например, больше чем 2 ^ 64?

Кто-нибудь даст мне несколько советов? Заранее спасибо.

2

c++z3

Решение

Другие решения

Вероятно, единственный ответ, который вы получите на этот вопрос: «Потому что разработчики сделали это так».

Мы действительно можем представлять только конечные величины в информатике. При разработке API иногда возникает вопрос, каким должно быть максимальное или минимальное значение чего-либо. В данном конкретном случае максимальное значение для n кажется UINT_MAX (есть unsigned int перегрузка для функции).

Может быть, разработчики подумали, когда n > UINT_MAX было нереально. Что никто в здравом уме не попытается.

Может быть, это потому, что выполнение операции с n > UINT_MAX был слишком обременителен для ресурсов (заняло слишком много времени, слишком много памяти).

Возможно, это потому, что есть способ разделить эту операцию на несколько частей, что делает невозможным выполнение ее за один большой проход.

Или, может быть, кто-то просто не подумал об этом и необходимость пройти n > UINT_MAX действительно существует. В этом случае, я полагаю, вы можете подать вопрос на их баг трекер.

Скорее всего, это просто потому, что кто-то подумал: «Достаточно хорошо». В любом случае, на этот вопрос невозможно ответить.

0

Источник

Accepted Answer

API Z3 C ++ предоставляет следующие методы для создания значений битовых векторов.

    expr bv_val(int n, unsigned sz);
expr bv_val(unsigned n, unsigned sz);
expr bv_val(__int64 n, unsigned sz);
expr bv_val(__uint64 n, unsigned sz);
expr bv_val(char const * n, unsigned sz);

Для значений битового вектора размером больше, чем UINTMAX64, мы должны использовать строки. Пример:

    expr big = ctx.bv_val("1267650600228229401496703205376", 512);

где ctx является контекстным объектом Z3

4