相关疑难解决方法(0)

我试图在 SMT-LIB 中表示时间约束，以检查它们的可满足性。我正在寻找有关我正在采取的方向的反馈。我对 SMT-LIB 比较陌生，我非常感谢输入。

我的限制是关于事件的时间和持续时间。例如，考虑以下自然语言中给出的约束：

1. 约翰从 13:03:41 开始写一篇文章，他花了 20 分钟才完成。

2. 写完之后，他检查了他的电子邮件，这花了他 40 多分钟。

3. 查完邮件后，他给妻子打了电话。

4. 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 …