Welche Logiken werden von z3 unterstützt?

Question

Gibt es eine vollständige Liste aller Theorien/Logiken, die z3 unterstützt? Ich habe diese SMTLIB Tutorial konsultiert, die eine Reihe von Logiken bietet, aber ich glaube nicht, dass die Liste erschöpfend ist. Die z3-Dokumentation selbst scheint nicht anzugeben, welche Logiken unterstützt werden.

Ich frage, weil ich eine SMT-Datei habe, die unter keiner der Logiken in der SMTLIB Tutorial gelöst werden kann (wenn mit 'Set-Logik' angegeben), kann aber gelöst werden, wenn keine Logik angegeben ist.

Answer 1

Für Z3 habe ich keine solche Liste in der Dokumentation gesehen, aber Sie können es im Quellcode finden, wenn Sie wirklich wissen wollen. Die Liste beginnt um Zeile 65 von check_logic.cpp. Ich analysiert, um die Liste für Sie eine beängstigende awk Einzeiler verwenden und fanden diese ab 20. Mai 2016 (zwischen Z3 4.4.1 und 4.4.2):

"AUFLIA", "AUFLIRA", "AUFNIRA", "LRA", "QF_ABV", "QF_AUFBV", "QF_UFBV", "QF_AUFLIA", "QF_AX", "QF_BV", "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", "QF_NIA", "QF_NRA", "QF_UF", "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", "QF_UFNRA", "UFLRA", "UFNIA", "UFBV", "QF_S"

Sie diese vergleichen können die offizielle Liste von SMT-LIB 2 logics.

Wahrscheinlich wichtiger für Sie ist, was die "beste Logik" für Ihre Anwendung ist. Es hört sich so an, als hättest du eine große und variierende Reihe von Problemen, von denen du willst, dass Z3 alle möglichen Taktiken anwendet. In diesem Fall ist es am besten, die Logik nicht näher zu spezifizieren. Das Problem ist, dass es in SMT-LIB v2.0 keine allumfassende Logik gab - die größte Logik einiger Standards war AUFNIRA, aber dies schließt beispielsweise keine Bitvektoren ein. Als Ergebnis führte CVC4 eine Nicht-Standard-ALL_SUPPORTED-Logik ein, und Z3 führt die beste Leistung für einige Klassen von Problemen durch, wenn keine Logik spezifiziert ist. Dieser Mangel des Standards SMT-LIB 2.0 wird in SMT-LIB 2.5 mit einer neuen Logik namens "ALL" angesprochen. Dies wird jedoch weder von Z3 noch von CVC4 unterstützt.

Answer 2

Sie geben eine Logik in Z3 an, um sicherzustellen, dass Z3 eine bestimmte Strategie und Engine verwendet, die normalerweise für die in dieser Logik ausgedrückte Klasse von Formeln nützlich ist. Wenn keine Logik angegeben ist, fällt Z3 in den Standardmodus zurück. Es gibt keine Logik, die diesem Standardmodus entspricht: es integriert mehrere Engines.