Как вырезать/подписать расширение битрейдеров в Z3?

Question

Мне не удалось выполнить нулевое расширение на битвектор с использованием интерфейса Z3 SMT. Из того, что я узнал, читая источники, для этого есть функции, и они доступны для различных привязок (C, C++, Python и т. Д.), Но учебник для интерфейса SMT не дает никакого представления о том, как их вызвать.

Использование zero_extend из логического стандарта SMT QF_BV тоже не помогает - Z3 говорит unsupported.

Answer 1

Оказалось, что zero_extend и некоторые другие функции параметрические те, вероятно, что-то вроде foo<T> в C++. Для вызова таких функций одной необходимости использовать специальный синтаксис:

(declare-const a (_ BitVec 1)) 
(declare-const b (_ BitVec 2)) 
(assert (= b ((_ zero_extend 1) a))) 
(check-sat) 
(get-model) 

Использование ((_ zero_extend i) x) вместо (zero_extend i x) дает правильный результат:

sat 
(model 
    (define-fun a() (_ BitVec 1) #b0) 
    (define-fun b() (_ BitVec 2) #b00) 
)