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

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

• http://www.logique.jussieu.fr/~point/papiers/Pres.pdf
• http://dx.doi.org/10.2307/2586704
• https://mathoverflow.net/questions/103896/beyond-presburger-arithmetic

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

Для ограниченных целых чисел, т. е. x в [a,b], где a и b — числа, поддержка конкретного решателя не предусмотрена, но вы можете смоделировать это. Сначала вы создаете константу skolem типа 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). Он использует линейное кодирование, подобное тому, которое дал Тим.