Объединение нелинейных вещественных и линейных чисел
Мы читали посты о нелинейных арифметических и неинтерпретированных функциях. Я'Я все еще очень новичок в мире 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 ...)
в зависимости от типов, которые были утверждены?