如何处理Z3中的递归函数? [英] How to deal with recursive function in Z3?

问题描述

(set-option :smt.mbqi true)
(declare-fun R(Int) Int)
(declare-const a Int)
(assert (= (R 0) 0))
(assert (forall ((n Int)) (=> (> n 0) (= (R n ) (+ (R (- n 1)) 1)))))
(assert (not (= a 5)))
(assert (not (= (R a) 5)))
(check-sat)

我已经在Z3中尝试了上面的代码，但是Z3无法回答.你能指导我哪里出错了吗?

I have tried the above code in Z3,But Z3 unable to answer.Can you please guide me where i have made the mistake ?

推荐答案

作为一般模式不要指望 MBQI 生成模型涉及的功能只有无限范围的不同值.如果你真的必须，那么你可以使用define-fun-rec构造来定义一个递归函数.Z3 目前相信定义是良构的(例如，对应于函数的方程定义是可满足的).

As a general pattern don't expect MBQI to produce models involving functions that only have an infinite range of different values. If you really must, then you can use the define-fun-rec construct to define a recursive function. Z3 currently trusts that the definition is well-formed (e.g., that the equation corresponding to the function definition is satisfiable).

(set-option :smt.mbqi true)
(declare-fun F (Int) Int)
(define-fun-rec R ((n Int)) Int
   (if (= n 0) 0
       (if (> n 0) (+ (R (- n 1)) 1)
            (F n))))

(declare-const a Int)
(assert (not (= a 5)))
(assert (not (= (R a) 5)))
(check-sat)
(get-model)

Z3 在搜索期间被动地使用递归定义的函数:每当约束的地面部分有一个候选模型，它检查函数图是否在候选模型的值上充分定义.如果不是，则在所选值上实例化函数定义，直到在相关值上很好地定义了它到地面限制.

Z3 uses recursively defined functions passively during search: whenever there is a candidate model for the ground portion of the constraints, it checks that the function graph is adequately defined on the values of the candidate model. If it isn't, then the function definition is instantiated on the selected values until it is well defined on the values that are relevant to the ground constraints.

这篇关于如何处理Z3中的递归函数?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！