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

Answer 1

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

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

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