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引擎來解決這些問題。