(check-sat-using default) oder ähnliches?

Question

Wenn Z3 ohne Logik ausgeführt wird und (check-sat) ausgegeben wird, wird die Logik in default_tactic.cpp verwendet, um den "besten" Löser bedingt aufzurufen. Ich möchte auf diese Standardtaktik von der SMT-LIB 2-Schnittstelle zugreifen.

Ich habe versucht, die Logik von default_tactic.cpp in SMT-LIB übersetzen, und ich kam mit dieser:

(check-sat-using (and-then simplify 
    (cond is-qfbv qfbv 
    (cond is-qflia qflia 
    (cond is-qflra qflra 
    (cond is-qfnra qfnra 
    (cond is-qfnia qfnia 
    (cond is-nra nra 
    (cond is-lira lira 
    (cond is-qffpabv qffpa 
    smt)))))))))) 

Dieses „fast“ funktioniert, dass, wenn Sie die Zeilen mit nra, löschen lira und qffpa, dann führt Z3 das ohne Problem aus. Es scheint, dass diese drei Taktiken nicht mit der SMT-LIB 2-Schnittstelle von Z3 4.4.1 offengelegt werden. Ein anderes Problem dabei ist, dass wenn die Standardtaktik in einer zukünftigen Version von Z3 aktualisiert wird, dann wird jede hartcodierte Strategie, wie sie oben geschrieben wurde, nicht aktualisiert.

Was ich wirklich gerne tun würde, ist einen Befehl wie (check-sat-using default), oder etwas ähnliches, und erhalten Sie das gleiche Ergebnis wie mit (check-sat) erhalten. Ist das möglich?

Answer 1

Die Datei, auf die Sie verweisen, ist sehr alt. Z3 wurde seitdem zu GitHub verschoben und die neueste Version von default_tactic.cpp ist here.

Die Standard-Taktik für QF_FP jetzt qffp genannt wird, hat sich die lira Taktik, da auch exportiert worden und ich exportiert nur nra als auch (wie von this commit).

---

Edit: Ab this commit, die default Taktik wird auch exportiert worden, so dass es nun möglich ist, (check-sat-using default) zu schreiben, wie angefordert.