2

解釈されない関数は 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

4

1 に答える 1

2

解釈されない関数はサポートされていません。代わりに配列で動作する場合もありますが、配列の処理はアドホックです (pdr エンジンには一般化ステップはありません)。おそらく、そのような問題には pdr エンジンも使用したいと思うでしょう。

于 2013-03-06T16:01:24.467 に答える