Przeczytałem posty o nieliniowych funkcjach arytmetycznych i nieinterpretowanych. Nadal jestem bardzo nowy w świecie SMT, więc przepraszam, jeśli nie używam właściwego słownictwa lub jest to złe pytanie.

W przypadku poniższego kodu na stosie znajdują się twierdzenia powyżej niepowiązanego asertu najwyższego poziomu,(assert (> i 10)). Jednak Z3 zwraca niesatysfakcjonujące wyniki w przypadku Realsa (pierwsze naciśnięcie do pierwszego popu). Myślę, że ma to coś wspólnego z próbą użycia przez Z3 solvera Int, ponieważ pierwsze twierdzenie było na Int, a Z3 przypisuje e1 do(/ 1.0 2.0), liczba bez reprezentacji Int, z powodu ograniczenia(assert (< e3 1)) (jeśli usunę to ograniczenie, działa). Za pomocą(check-sat-using qfnra-nlsat) rozwiązuje problem dla Reals, ale wracaunknown w przypadku Ints, jednak wciąż mogę uzyskać model dla przypadku Int, który spełnia ograniczenia.

(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)

Czy istnieje pojedynczy telefon, aby sprawdzić, czy mogę użyć we wszystkich przypadkach, czy będę musiał użyć(check-sat-using ...) w zależności od typów, które zostały potwierdzone?