Создание ограничения маски переменной ширины в Z3 - PullRequest
Новая
       21

Создание ограничения маски переменной ширины в Z3

0 голосов
/ 24 июня 2019

Я хотел бы создать ограничение для битового вектора (X), который маскирует другой битвектор к его n младшим значащим битам. Я бы хотел, чтобы это было максимально эффективно. До сих пор я пытался представить второй битовый вектор как: 1<<n - 1, где n - другой битовый вектор. Это дает мне две проблемы:

  • Во-первых, это сильно замедляет решатель
  • Во-вторых, и, возможно, в связи с первым, я не могу установить ширину n меньше ширины X. Если я это сделаю, то произойдет сбой с ошибкой типа на n.

Есть идеи для более эффективного подхода к решению проблемы ширины?

1 Ответ

1 голос
/ 24 июня 2019

Не совсем понятно, что вы пытаетесь сделать, размещение реального кода всегда более полезно. Но, исходя из вашего описания, вы можете просто сместить сначала влево, а затем снова вправо. Это подтолкнет 0 снизу, а затем сбросит их; убедившись, что в битовом векторе осталось наименьшее количество n битов. Величина, которую вы сдвигаете, должна быть равна bitsize - n, где bitsize - это длина ваших битовых векторов, а n - это сколько младших битов вы хотите сохранить. Предполагая, что вы имеете дело с 64-битными векторами, это будет выглядеть примерно так: 

(declare-const n (_ BitVec 64))
(declare-const x (_ BitVec 64))
(define-fun amnt () (_ BitVec 64) (bvsub #x0000000000000040 n))
(define-fun maskedX () (_ BitVec 64) (bvlshr (bvshl x amnt) amnt))

(Константа #x0000000000000040 - это то, как вы пишете 64 в SMT-lib как 64-битную константу битового вектора.) Обратите внимание, что это неявно предполагает, что n самое большее 64: если это не так, то вычитание обернется, и вы получите другое ограничение. Я предполагаю, что в вашей системе уже есть ограничение, которое говорит, что n имеет максимальный размер битового вектора, с которым вы имеете дело.

Относительно эффективности: на самом деле не существует очевидного способа сделать ограничения битового вектора такими, быстрыми или медленными: это действительно зависит от других ограничений, которые у вас есть. Поэтому невозможно определить, является ли это наилучшим способом достижения того, чего вы хотите, не зная ничего о вашей проблеме. Обычно бесполезно думать о «скорости» в SMTLib, когда присутствуют символические значения, существует так много факторов, которые влияют на эффективность решателя.

Относительно типов: SMTLib основан на очень простой системе типов первого порядка. Итак, да: почти все битовые векторные операции должны иметь точно такие же размеры, что и аргументы. Это сделано по замыслу: битовые векторы переменной длины просто не доступны в логике, так как это сделает его бесполезным, поскольку выполнимость формул будет зависеть от фактических размеров битов, для которых вы их создаете.

Если это не поможет, я бы рекомендовал опубликовать реальный фрагмент кода того, что вы пытаетесь сделать, и проблемы, с которой вы столкнулись. Чем конкретнее пример, тем лучше.

...