Próbuję użyć Z3 do określenia, czy wyrażenie jest zadowalające. Mogę to łatwo zrobić, definiując kontekst, a następnie zmienne int_const i formułę. Aby programowo ocenić wyrażenie, musisz napisać wszystko w kodzie. Powiedzmy, że wyrażenie logiczne jest podane w postaci ciągu, co wtedy? Na przykład,

„x == y &&! x == z”

byłby wyrażony w C API jako:

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

Dobra, mogę napisać kod dla tej konkretnej formuły, ale jak mogę to zrobić programowo, podając ciąg. Jestem otwarty na wszystko, o czym myślisz.

Dziękuję Ci :)