我试图在 SMT-LIB 中表示时间约束,以检查它们的可满足性。我正在寻找有关我正在采取的方向的反馈。我对 SMT-LIB 比较陌生,我会非常感谢您的投入。
我的限制是关于事件的时间和持续时间。例如,考虑以自然语言给出的以下约束:
约翰在 13:03:41 开始写一篇文章,他花了 20 分钟完成。
写完后,他查看了他的电子邮件,这花了他 40 多分钟。
在查看了他的电子邮件后,他给他的妻子打电话。
14:00:00后,他给妻子打电话。
很容易看出,这组约束是 staisfiable 的,我正在尝试使用 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)
)
Getter 是使用宏定义的,允许我们检索特定的度量,例如:
(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 中定义这种类型的时间约束的并行工作。我真的很感谢对现有作品的引用。
谢谢!