Вдохновленный вопросом , связанным с SMT2 , я пытаюсь связать Bool переменные с битами BitVector.
Упрощенный пример:
(declare-fun a () Bool)
(declare-fun v () (_ BitVec 2))
(assert (= ((_ extract 0 0) v) (ite a #b1 #b0)))
Я должен связать несколько сотен переменных с векторами. Моя цель - использовать ограничения BitVector довольно компактно.
Действительно ли необходимо прибегнуть к ite вызову map между BitVectors переменных длины 1 и Bool?