Estou tentando usar o Z3 para determinar se uma expressão é satisfatória. Eu poderia facilmente fazer isso definindo o contexto e as variáveis ​​int_const e a fórmula. Para avaliar uma expressão programaticamente, você teria que escrever tudo no código. Digamos que a expressão lógica seja dada na forma de uma string, e depois? Por exemplo,

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

seria expresso na API 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

Ok, eu posso escrever o código para esta fórmula particular, mas como eu poderia fazer isso de forma programática dada uma string. Estou aberto a qualquer coisa que você possa pensar.

Obrigado :)