Unterstützt Z3py "String" und "Sequence"

Question

In Z3 unterstützt String und Sequenz. Aber unterstützt Z3py sie auch, oder müssen wir String oder Liste aus Python verwenden? Seit der letzten Version scheint es, dass die neue Version die Theorien von String und Sequence unterstützt, aber ich weiß nicht, wie ich sie verwenden soll. Würde mir jemand ein Beispiel für die Sequenz geben?

Answer 1

Ja, Z3 unterstützt Strings und Sequenzen, aber in der letzten öffentlichen Version gibt es nur rudimentäre Unterstützung. Sie müssen den neuesten Master aus der Quelle kompilieren, um alle Funktionen zu erhalten (einschließlich der Python-API).