Estoy tratando de usar Z3 para determinar si una expresión es satisfactoria. Podría hacerlo fácilmente definiendo el contexto y luego las variables int_const y la fórmula. Para evaluar una expresión mediante programación, tendría que escribir todo en código. Digamos que la expresión lógica se da en forma de una cadena, ¿entonces qué? Por ejemplo,

"x == y &&! x == z"

Se expresaría en la API de C como:

context c;
expr x = c.int_const("x")
//Same for other variables
...
formula = (x == y) && (!x == z);
solver s(c);
s.add(formula);
//s.check() ...etc etc

Está bien, puedo escribir el código para esta fórmula en particular, pero ¿cómo podría hacer eso mediante una cadena programada? Estoy abierto a cualquier cosa que se pueda imaginar.

Gracias :)