文章/答案/技术大牛

发布

社区首页 >问答首页 >如何在SMTLIB / Z3 / CVC4中声明所有限定符？

问如何在SMTLIB / Z3 / CVC4中声明所有限定符？
EN

Stack Overflow用户

提问于 2021-04-15 06:21:41

回答 1查看 83关注 0票数 2

我一直纠结于如何在SMTLIB2中创建断言如下的语句

forall x < 100, f(x) = 100

此属性将检查递归地将所有小于100的数字加1的函数：

(define-fun-rec incUntil100 ((x Int)) Int  
    (ite 
        (= x 100) 
        100
        (incUntil100 (+ x 1))
    )
)

我通读了一遍Z3 tutorial on quantifiers and patterns，但似乎对我没什么帮助。

回答已采纳

发布于 2021-04-15 06:30:17

在SMTLib中，您可以按如下方式编写该属性：

(assert (forall ((x Int)) (=> (< x 100) (= (incUntil100 x) 100))))
(check-sat)

但是如果您尝试这样做，您将看到z3将永远循环，并且CVC4将告诉您unknown作为答案。虽然您可以在SMTLib中定义和断言这些类型的函数，但求解器对实际证明的支持相当弱，因为它们不做开箱即用的归纳。

如果你的目标是证明递归函数的性质，那么SMT求解器不是一个好的选择；相反，看看定理证明器，比如Isabelle，HOL，Coq，Lean，ACL2等等，它们就是为这个目的而构建的。

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/67099826

复制

相似问题

问如何在SMTLIB / Z3 / CVC4中声明所有限定符？EN