Z3 не решает выражение квантора, выражение выполнено
Используя z3 v 4.8.1 - - 64-разрядный - сборка хэш-кода 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)
Ответы 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, которые удовлетворяли бы этому для ВСЕ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, ответив на другой вопрос.