Cómo resolver restricciones con variables booleanas y bitvectores en la interfaz C / C ++ de STP

Question

Supongamos que tengo las siguientes restricciones

(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun t1 () (_ BitVec 8))
(declare-fun t2 () (_ BitVec 8))
(assert (or x y))
(assert (=> x (bvule t1 t2)))
(assert (=> y (bvule t2 t1)))
(check-sat)

¿Cómo escribir el código correspondiente en la interfaz C / C ++ de STP? Mi aplicación requiere resolver un conjunto de restricciones similares a esto. Cualquier ayuda es apreciada.

Answer 1

Consulte la encabezado de interfaz C para cómo construir diferentes operadores.