Объединение нелинейных вещественных и линейных чисел

Question

Я читал посты о нелинейной арифметике и неинтерпретируемых функциях. Я все еще очень плохо знаком с миром SMT, поэтому извиняюсь, если я не использую правильный словарный запас или это плохой вопрос.

Для следующего кода есть утверждения, помещенные в стек над несвязанным утверждением верхнего уровня, (assert (> i 10)), Тем не менее, Z3 возвращает unsat для случая с Reals (первый толчок к первому трепу). Я думаю, что это как-то связано с попыткой Z3 использовать решатель Int, так как первое утверждение было в Int, а Z3 назначает e1 (/ 1.0 2.0), число без представления Int из-за ограничения (assert (< e3 1)) (если я уберу это ограничение, оно будет работать). С помощью (check-sat-using qfnra-nlsat) решает проблему для Реалов, но возвращает unknown для случая Ints, однако, я все еще могу получить модель для случая Int, которая удовлетворяет ограничениям.

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

Есть ли один вызов, чтобы проверить, что я могу использовать во всех случаях, или мне нужно будет использовать (check-sat-using ...) в зависимости от типов, которые были утверждены?

Answer 1

Поскольку вы смешиваете реальные и целочисленные сортировки, я думаю, вам нужно использовать check-sat-using, Из Как Z3 обрабатывает нелинейную целочисленную арифметику?:

"Нелинейный реальный арифметический решатель (NLSat) по умолчанию не используется для нелинейных целочисленных задач. Он обычно очень неэффективен для целочисленных задач. Тем не менее, мы можем заставить Z3 использовать NLSat даже для целочисленных задач".

Вы заставляете Z3 использовать нелинейный реальный арифметический решатель на целочисленных ограничениях с (check-sat-using qfnra-nlsat), Вот также, как сделать это в Python с z3py: z3 не работает с этой системой уравнений

Я думаю, что в какой-то момент в будущем (хотя разработчики могут подтвердить), вам не придется делать это, но последнее, что я услышал (см., Например, смешение реалов и битовых векторов и использование Z3Py онлайн, чтобы доказать, что n^5 <= 5 ^n для n>= 5), тактика нелинейного вещественного арифметического решателя еще не полностью интегрирована с другими решателями.