Шаги дискретного времени в Z3/CVC4/SMT-LIB

Я определяю временные шаги, используя Int в SMT-LIB, что заставляет меня утверждать вещи, чтобы убедиться, что ничего не происходит в отрицательных значениях:

(declare-sort Pkg) ; A package
(define-sort Time () Int) ; The installation step
; ...
(assert (forall ((t Time) (p Pkg)) (=> (< t 0) (not (installed p t)))))

Я видел, что в Z3 мы можем определить индуктивные Nat в обычном стиле. Было бы хорошо использовать индуктивное определение Nat или есть лучший способ сделать то, что я пытаюсь сделать выше?


z3 smt cvc4
person buggymcbugfix    schedule 02.03.2018    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы действительно должны придерживаться Int и правильно вводить ограничения >= 0. Z3 много знает о Int, имеет всевозможные правила проверки и приемы для работы с ним. Хотя вы действительно можете определить индуктивный тип Nat, вы потеряете весь внутренний механизм для работы с целыми числами, а из-за рекурсивного определения процедуры принятия решений Z3 будут менее эффективными; особенно в сочетании с другими теориями.

Сказав это, невозможно узнать, если вы не попробуете: могут быть некоторые проблемные области, где индуктивное определение может подойти лучше. Но если просто посмотреть на проблему, с которой вы имеете дело, старый добрый Int кажется правильным выбором для вас.

Также см. этот связанный вопрос: Представление временных ограничений в SMT-LIB, что определенно актуально в вашем контексте.

person alias    schedule 02.03.2018
comment
Спасибо за ваш взгляд. Я видел вопрос, на который вы ссылались (Представление временных ограничений), но я не уверен, как бы я использовал Reals в моем случае, потому что я смотрю на дискретные шаги, как в конечном автомате. Если мне все-таки удастся использовать реалы, я отпишусь, как все прошло. - person buggymcbugfix; 03.03.2018