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。使用Nat的归纳定义是不是很好，或者有没有更好的方法来做我上面试图做的事情？

Answer 1

您真的应该坚持使用Int，并适当地添加>= 0约束。Z3对Int了解很多，有各种各样的证明规则和技巧来处理它。虽然您确实可以定义归纳Nat类型，但您将失去处理整数的所有内部机制，而且由于递归定义，Z3的决策过程将不那么有效；特别是在与其他理论结合时。

话虽如此，除非你尝试一下，否则是不可能知道的:可能有一些问题领域，归纳定义可能更适合。但仅从您处理的问题的类型来看，良好的旧Int似乎是适合您的正确选择。

另请参阅这个相关的问题：Representing temporal constraints in SMT-LIB，它肯定与您的上下文相关。