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

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

Джон начал писать сочинение в 13:03:41, и ему потребовалось 20 минут, чтобы закончить его.

После написания он проверил свою электронную почту, что заняло у него более 40 мин.

После проверки своей электронной почты он позвонил своей жене.

Он позвонил своей жене после 14:00:00.

Легко видеть, что этот набор ограничений является устойчивым, и я пытаюсь вывести это с помощью решателя SMT.

Чтобы иметь некоторую инкапсуляцию для понятий времени и продолжительности, я определил новые сорта, которые представляют их в массивах. Некоторые макросы были определены для работы в качестве конструкций:

(define-sort Time () (Array Int Int))
(define-fun new_time_ns ((hours Int) (minutes Int) (seconds Int) (nanos Int)) Time
    (store (store (store (store ((as const (Array Int Int)) 0) 1 hours) 2 minutes) 3 seconds) 4 nanos)
)
(define-sort Duration () (Array Int Int))
(define-fun new_duration_ns ((seconds Int) (nanos Int)) Duration
    (store (store ((as const (Array Int Int)) 0) 1 seconds) 2 nanos)
)

Получатели определяются с помощью макросов и позволяют нам извлекать конкретные меры, например:

(define-fun getDurationSecond ((d Duration)) Int
  (select d 1)
)

(define-fun getDurationNano ((d Duration)) Int
  (select d 2)
)

Некоторые служебные макросы были определены для арифметики времени и продолжительности и для выражения отношений. Например, используя некоторые вспомогательные макросы, мы определяемisLongerThan, isShorterThan а такжеisEqualDuration следующее:

(define-fun cmpInt ((i1 Int) (i2 Int)) Int
  (ite (< i1 i2) -1 (ite(> i1 i2) 1 0))
) 

(define-fun cmpDuration ((d1 Duration) (d2 Duration)) Int
  (ite (= (cmpInt (getDurationSecond d1) (getDurationSecond d2)) 0) 
    (ite (= (cmpInt (getDurationNano d1) (getDurationNano d2)) 0)
    0
    (cmpInt (getDurationNano d1) (getDurationNano d2)))
  (cmpInt (getDurationSecond d1) (getDurationSecond d2)))
)  

(define-fun isLongerThan ((d1 Duration) (d2 Duration)) Bool
  (> (cmpDuration d1 d2) 0)
)

(define-fun isShorterThan ((d1 Duration) (d2 Duration)) Bool
  (< (cmpDuration d1 d2) 0)
)

(define-fun isEqualDuration ((d1 Duration) (d2 Duration)) Bool
  (= (cmpDuration d1 d2) 0)
)

Остальные определения можно найти вэтот файл.

На основании этого я могу выразить ограничения набором утверждений:

(declare-const write_start Time)
(declare-const write_end Time)
(declare-const write_duration Duration)

(declare-const check_start Time)
(declare-const check_end Time)
(declare-const check_duration Duration)

(declare-const phone_start Time)

(assert (= write_start (new_time_ns 13 03 41 0)))  ; the writing started at 13:03:41
(assert (= write_duration (new_duration 1200)))    ; the writing took 20 min (1200 sec).
(assert (= write_end (plusDuration write_start write_duration)))

(assert (isAfter check_start write_end))                   ; the check started after the writing
(assert (isLongerThan check_duration (new_duration 2400))) ; the check took more than 40 min
(assert (= check_end (plusDuration check_start check_duration)))

(assert (isAfter phone_start check_end))                   ; he phoned after the check
(assert (isAfter phone_start (new_time_ns 14 00 00 0)))    ; it was after 14:00:00

(check-sat)

Некоторые вопросы и проблемы:

В плане дизайна мне было бы интересно узнать, является ли это разумным моделированием проблемы в SMT-LIB.

Некоторые примечания, которые нужно добавить здесь: (A) Я решил использовать массивы для представления объектов времени и продолжительности, поскольку они помогают сгруппировать внутренние поля этих концепций (часы, минуты, секунды, наночастицы). Отдельные целые числа могут быть использованы так же хорошо. (B) Я очень сильно полагаюсь на макросы (define-fun ...), и это может усложнить ограничения, но я не знаю, что еще можно использовать для достижения требуемого уровня выразительности и ясности что текущий код имеет. (C) В настоящее время нет ограничений, ограничивающих временные поля, поэтому, например, значение поля минут может быть 78. Следует добавить утверждения, которые ограничивают секунды 59, минуты 59 и часы 23 , но я не нашел элегантного способа сделать это.

Я предполагаю, что я нахожусь в разрешимом фрагменте FOL - QF_LIA - так как все ограничения объявлены с использованием линейных функций над целочисленными константами. Тем не менее, я пытался бежатьприкрепленный код через Z3 и даже после 40 минут локальной работы на среднем компьютере он все равно не возвращается с разрешением (sat / unsat). Я действительно не знаю, может ли это вообще решить проблему. Возможно, мое предположение о нахождении в QF-LIA неверно, а также возможно, что Z3 борется с этим типом ограничений. Я могу добавить, что когда я попробовал более простые ограничения, Z3 удалось достичь разрешения, но я заметил, что сгенерированные им модели были очень сложными с множеством внутренних структур. Может кто-нибудь, пожалуйста, дайте мне несколько идей для расследования здесь? Z3 онлайн-доказательство с моим кодом можно найтиВот, Я еще не пробовал другие решения для SMT.

Я не знаю о параллельных работах, которые пытаются определить временные ограничения этого типа в SMT-LIB. Буду очень признателен за ссылки на существующие работы.

Спасибо!