Я очень новичок в Z3 и пытаюсь использовать его bitvector C++ API. Насколько я понял, метод bv_val (int n, unsigned sz) в контексте класса ставит целью создать битвектор размера sz со значением n. Но почему значение n ограничено типом int?. Что произойдет, если я создам битвектор размера 10 со значением, например. более 2^64?Создать постоянный битвектор
Может кто-нибудь даст мне несколько предложений? Заранее спасибо.
Z3 C++ API предоставляет следующие методы для создания значений вектора бит.
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 объект контекста.
Большое спасибо за ответ. Я не знал, что существует также метод 'expr bv_val (char const * n, unsigned sz);'. –
Вероятно, единственный ответ, который вы получите на этот вопрос: «Потому что разработчики сделали это так».
Мы действительно можем представлять только конечные величины в информатике. При разработке API иногда возникает вопрос о том, какой должна быть максимальная или минимальная ценность чего-либо. В этом конкретном случае максимальным значением для n является UINT_MAX (есть функция перегрузки unsigned int).
Возможно, разработчики подумали, что прецедент, где n > UINT_MAX был нереалистичным. Что никто в здравом уме не попытается это сделать.
Возможно, это связано с тем, что выполнение операции с n > UINT_MAX было слишком обремененным ресурсами (заняло слишком много времени, слишком много памяти).
Возможно, это потому, что есть способ разделить этот вид операции на несколько частей, что делает невозможным выполнить его в одном большом проходе без проблем.
Или, может быть, кто-то просто не думал об этом и необходимость пройти n > UINT_MAX действительно существует. В этом случае, я считаю, вы можете отправить вопрос на свой bug tracker.
Скорее всего, это просто потому, что кто-то подумал: «Достаточно хорошо». В любом случае на этот вопрос нельзя ответить.
С каких это пор 10 больше, чем 2^64? –
Я не знаю 'Z3', но я предполагаю и говорю:« Не заполняйте материал больше, чем его емкость ». Вопрос: «Чего вы хотите достичь?». Мы можем вам помочь – stefan
Путаница о том, указан ли размер в битах или байтах (или что-то еще)? –