Есть ли какая-либо функция для расчета логарифма по основанию 2 в Z3/cvc4?

Я хочу доказать упрощение, которое включает вычисление log для базы 2. Есть ли в z3/cvc4 какая-либо функция для ее вычисления?

Источник

2 ответа

Решение

Короткий ответ: поддержка недоступна для целых чисел ни в одном инструменте. Для неограниченных целых чисел существуют процедуры принятия решений для возведения в степень Пресбургера фиксированной константой. Из этого вы можете построить функцию логарифма (или наоборот). Я не эксперт, но я понимаю, что это довольно сложно. Для дополнительной информации:

Я не знаю ни о какой существующей реализации этих алгоритмов.

Для ограниченных целых чисел, т. Е. X в [a,b], где a и b - цифры, не существует решающей поддержки, но вы можете смоделировать это. Сначала вы создаете константу сколем s типа Integer. Затем вы форсируете интерпретацию s, используя утверждение:

(and (=> (2^0 <= x < 2^1)  (= s 0))
     (=> (2^1 <= x < 2^2)  (= s 1))
     ...
     (=> (2^i <= x < 2^{i+1}) (s = i)) ; for all 2^i in [a,b] and i >= 0.
)

Это не интерпретирует s, если x <= 0 (что я считаю разумным). Это очень неудовлетворительно, но оно линейно. (Если кто-то знает лучшую кодировку, я хотел бы знать об этом!) Вы также можете кодировать вышеуказанные аксиомы, используя квантификаторы для ограниченных или неограниченных целых чисел. Сначала вы кодируете функцию 2^i как неинтерпретируемую функцию, используя квантификаторы. Затем вы определяете функцию журнала, используя функцию 2^i. Это может привести к тому, что решатель вернет неизвестное, и вам, вероятно, придется поиграть с опциями решателя для модулей квантификаторов, если вы пойдете по этому пути.

Для битовых векторов вам необходимо решить, являются ли числа знаковыми или беззнаковыми. Для значений без знака длины k вы можете смоделировать это с помощью правого сдвига.

(=> (bvugt x (_ bv0 k)))  (= (bvlshr x s) (_ bv1 k))

Снова x <= 0 (без знака) не интерпретируется. Подписанные битовые векторы похожи:

(=> (bvsgt x (_ bv0 k)))  (= (bvlshr x s) (_ bv1 k))
Источник

В Alive действительно есть функция log2(foo). Он использует линейное кодирование, подобное тому, которое дал Тим.

Источник
Другие вопросы по тегам