Z3 / CVC4 / SMT-LIB 中的离散时间步长

Question

我在 SMT-LIB 中使用 Int 定义时间步长，这迫使我断言事情以确保在否定中没有任何事情发生：

(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 中我们可以用通常的样式定义归纳Nats。使用Nat 的归纳定义会更好还是有更好的方法来做我上面想做的事情？

Answer 1

你真的应该坚持Int，并适当地放入>= 0约束。 Z3对Int非常了解，有各种证明规则和技巧来应对。虽然您确实可以定义一个归纳Nat 类型，但您将失去处理整数的所有内部机制，并且由于递归定义，Z3 的决策过程将不太有效；尤其是结合其他理论。

话虽如此，除非您尝试，否则不可能知道：可能存在一些问题域，其中归纳定义可能更适合。但仅从您遇到的问题来看，老旧的Int 似乎是您的正确选择。

另请参阅此相关问题：Representing temporal constraints in SMT-LIB，这绝对与您的上下文相关。