Z3 muZ + 未解释的函数？

Question

muZ 是否支持未解释的函数？

我想做如下的事情:

(declare-fun f (Int) Int)
(declare-rel r (Int))
(declare-var X Int)
(rule (=> (= (f X) X) (r X)))
(query (r X)
:default-relation smt_relation2
:engine datalog
:print-answer true)

但似乎我需要为 f 提供定义，因为 Z3 返回以下输出:

% z3 -smt2 test.z3
error "query failed: Uninterpreted 'f' in r(#0) :- 
(= (f (:var 0)) (:var 0)).
")
unknown

我认为我可以将函数建模为关系，但想看看是否还有其他解决方法......

谢谢!

-N

Answer 1

不支持未解释的函数。在某些情况下，它会使用数组，但数组的处理是临时的(pdr 引擎中没有泛化步骤)。您可能还想使用 pdr 引擎来解决此类问题。