z3 - 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 引擎来解决此类问题。