Ich musste den Wert eines Ausdrucks mit Z3 über verschiedene Variablenwerte auswerten. Ich weiß, dass Z3 ein Zufriedenheitsprüfer ist, aber model.Eval (Args) bewirkt Auswertungen eines Ausdrucks bei Werten von Variablen, die vom Modell generiert werden.

Es ist uns also möglich, verschiedene Werte zu durchlaufen, um einen Ausdruck zu bewerten.

Beispiel: p und q bei allen möglichen Werten von p und q (p, q ist Boolesch)

In gewisser Weise kann man eine Wahrheitstabelle daraus erstellen, indem man eine Rekursion oder Iteration verwendet. Kann Z3 das auch?

Die Hilfe mit der C # -API wird noch besser.

Vielen Dank