Z3 не решает выражение квантификатора, выражение сат

Question

Используя z3 v 4.8.1 - - 64 bit - build hashcode 016872a5e0f6, приведенный ниже скрипт оценивается как unsat, но ожидается результат sat.

• Поддерживает ли z3 решение таких выражений?

• Может ли другой smt-solver решать такие выражения?

  (set-option :print-success false)
  (set-logic ALL)
  (push 1)
  (declare-const ss1 Int)
  (declare-const ss3 Int)
  
  (assert (forall ((t_ss3 Int)(t_ss1 Int))
  (=>
    (< t_ss1 t_ss3)
    (and (and
     (< ss1 ss3)
     (= t_ss1 ss1))
     (= t_ss3 ss3))
  )))
  (echo "Check if the P -> Q is satisfiable")
  (check-sat)
  (pop 1)
  

Answer 1

Z3 здесь правильно; Сценарий, который вы изложили, действительно unsat. Вот что вы сказали:

• Пусть будет две константы ss1 и ss3

• Для всех целых чисел t_ss3 и t_ss1 всякий раз, когда выполняется t_ss1 < t_ss3, должно быть так:

  • ss1 < ss3
  • И, t_ss1 равно ss1
  • И, t_ss3 равно ss3

Это явно не так для всех t_ss1 и t_ss3. Не существует ss1 и ss3, которые бы удовлетворяли этому для ALL t_ss1 и t_ss2. Вам нужно только взглянуть на самое последнее предложение: вы не можете ожидать, что все t_ss3 будут равны произвольным ss3.

Я подозреваю, что вы пытаетесь выразить какое-то другое свойство; но вы не правильно его кодировали. Может быть, вы пытались сказать, если t_ss1 равно ss1 и t_ss3 равно ss3 и t_ss1 < t_ss3, тогда ss1 < ss3? Это будет закодировано следующим образом:

(declare-const ss1 Int)
(declare-const ss3 Int)

(assert (forall ((t_ss3 Int) (t_ss1 Int))
        (=> (and (< t_ss1 t_ss3)
                 (= t_ss1 ss1)
                 (= t_ss3 ss3))
            (< ss1 ss3))))

(check-sat)

и действительно даст sat.

Если вы придумаете лучшее описание того, что вы пытаетесь выразить, вы можете получить лучшую помощь в его моделировании в SMT-Lib по другому вопросу.