Добавление ограничений на целочисленные биты в Z3 - PullRequest
Новая
       106

Добавление ограничений на целочисленные биты в Z3

1 голос
/ 20 февраля 2020

У меня есть целочисленная константа, скажем: 

expr x = ctx.int_const("x");

Я пытаюсь применить случайные ограничения к отдельным битам x. Однако оказывается, что вы не можете использовать побитовые операции с целочисленными сортировками, только битовые векторы. Мой первоначальный подход до реализации этого был такой: 

for(int i = 0; i < 32; i++){
    int mask = 0x00000001 << i;
    if(rand()%2)
        solver.add((x & mask) == 0);
    else
        solver.add((x & mask) != 0);
}

Это, конечно, не работает, поскольку Z3 создает исключение. Немного покопавшись в API, я нашел функцию Z3_mk_int2bv и решил, что попробую: 

for(int i = 0; i < 32; i++){
    if(rand()%2)
        solver.add(z3::expr(ctx(),Z3_mk_int2bv(ctx(), 32, v())).extract(i, i) == ctx().bv_val(0, 1));
    else
        solver.add(z3::expr(ctx(),Z3_mk_int2bv(ctx(), 32, v())).extract(i, i) != ctx().bv_val(0, 1));
}

Хотя на вышеупомянутые решающие вызовы add не добавляется утверждение, фактическое Время решения внезапно взорвалось. Настолько, что мне еще предстоит увидеть, сколько на самом деле это займет времени. Добавление похожих выражений с использованием битовых векторов не требует больших затрат на SAT-решателе, поскольку время решения, насколько я могу судить, составляет менее секунды.

Мне интересно, что это за выражение выше что может привести к такому ухудшению производительности решателя, и есть ли лучший подход?

1 Ответ

2 голосов
/ 20 февраля 2020

int2bv дорого. Для этого есть много причин, но теперь решающий вопрос должен договориться между теорией целых и битовых векторов, и эвристика, вероятно, мало чем поможет. Обратите внимание, что для правильного преобразования решатель должен выполнить повторные деления, что довольно дорого. Кроме того, говорить о битах математического целого числа не имеет большого смысла, чтобы начать с: что, если это отрицательное число? Предполагаете ли вы что-то вроде представления дополнения бесконечной ширины 2? Или это какое-то другое отображение? Все это усложняет рассуждения о таких преобразованиях. И долгое время int2bv не интерпретировалось в z3 по этой и аналогичным причинам. Вы можете найти много сообщений об этом по переполнению стека, например, здесь: Z3: Вопросы о Z3 int2bv?

Лучше всего было бы просто использовать битовые векторы, чтобы начать с , Если вы рассуждаете о машинной арифметике c, почему бы не смоделировать все с битовыми векторами для начала?

Если вы застряли с типом Int, я бы порекомендовал просто придерживаться функции mod, убедившись, что второй аргумент является константой. Это могло бы избежать некоторых сложностей, но, не глядя на реальные проблемы, трудно продолжить обсуждение.

...