Ich habe die Posts über nichtlineare arithmetische und nicht interpretierte Funktionen gelesen. Ich bin noch sehr neu in der SMT-Welt, entschuldige mich, wenn ich nicht den richtigen Wortschatz verwende oder dies eine schlechte Frage ist.

Für den folgenden Code gibt es Asserts, die über einem nicht verwandten Assert der obersten Ebene auf den Stapel gelegt werden.(assert (> i 10)). Z3 kehrt jedoch für den Fall mit Reals (dem ersten Push zum ersten Pop) unbefriedigt zurück. Ich denke, dies hat etwas mit dem Versuch von Z3 zu tun, einen Int-Löser zu verwenden, da die erste Behauptung auf einem Int war und Z3 e1 zuweist(/ 1.0 2.0)Eine Zahl ohne Int-Darstellung aufgrund der Einschränkung(assert (< e3 1)) (Wenn ich diese Einschränkung aufhebe, funktioniert es). Verwenden(check-sat-using qfnra-nlsat) löst das Problem für Reals, kehrt aber zurückunknown für den Fall von Ints kann ich jedoch immer noch ein Modell für den Int-Fall erhalten, das die Einschränkungen erfüllt.

(set-option :global-decls false)

(declare-const i Int)
(assert (> i 10))

(push)
  (declare-const e1 Real)
  (declare-const e2 Real)

  (define-fun e3 () Real (/ e1 e2))
  (assert (> e1 0))
  (assert (> e2 0))
  (assert (< e3 1))

  ;(check-sat-using qfnra-nlsat)
  (check-sat)
(pop)
(push)
  (declare-const e1 Int)
  (declare-const e2 Int)

  (define-fun e3 () Int (div e1 e2))
  (assert (> e2 0))
  (assert (> e3 0))

  ;(check-sat-using qfnra-nlsat)
  (check-sat)
(pop)

Gibt es einen einzigen Anruf, um zu überprüfen, ob ich ihn in allen Fällen verwenden kann, oder muss ich ihn verwenden?(check-sat-using ...) abhängig von den Typen, auf die behauptet wurde?