1

2 つの未解釈の関数 func1 と func2 があるとします。

stuct_sort func1(struct_sort);
stuct_sort func2(struct_sort ,int).

そして、それらには次の関係があります。

func2(p,n)=func1(p)  if n==1
func2(p,n)=func1(func2(p,n-1))  if n>1

私が知りたいのは、次の命題の場合：

((forall i:[1,m].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,m-1].func2(q,i)==Z)

Z3 で真であると証明できますか? 私のプログラムでは、証明結果はZ3_L_UNDEFです。

m に 3 などの値を代入すると、命題は次のようになります。 

((forall i:[1,3].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,3-1].func2(q,i)==Z);

結果はZ3_L_UNDEFです。しかし、次のようにケースを個別に（forallを使用せずに）書き直すと、結果はtrue.

(func2(p,1)==Z)&&(func2(p,2)==Z)&&(func2(p,3)==Z)&&(q==func1(p)) implies (func2(q,1))&&(func2(q,2)).

原因がわかりません 回答お待ちしております

4

1 に答える 1

1

Z3 Python インターフェイスを使用して問題をエンコードし、Z3 が解決しました。予想の反例が見つかりました。もちろん、問題をエンコードしたときに間違いを犯した可能性があります。Python コードは記事の最後にあります。rise4funでオンラインで試すことができます。ところで、Z3 のどのバージョンを使用していますか? C API を使用していると仮定しています。その場合は、Z3 式を作成するために使用した C コードを提供していただけますか? もう 1 つの可能性は、アプリケーションと Z3 の対話を記録するログを作成することです。ログ ファイルを作成するにはZ3_open_log("z3.log");、他の Z3 API を実行する前に実行する必要があります。ログ ファイルを使用して、アプリケーションと Z3 の間のすべてのやり取りを再生できます。

from z3 import *
# Declare stuct_sort 
S = DeclareSort('stuct_sort')
I = IntSort()
# Declare functions func1 and func2
func1 = Function('func1', S, S)
func2 = Function('func2', S, I, S)

# More declarations
p = Const('p', S)
n = Int('n')
m = Int('m')
i = Int('i')
q = Const('q', S)
Z = Const('Z', S)

# Encoding of the relations 
#    func2(p,n)=func1(p)  if n==1
#    func2(p,n)=func1(func2(p,n-1))  if n>1
Relations = And(func2(p, 1) == func1(p), 
                ForAll([n], Implies(n > 1, func2(p, n) == func1(func2(p, n - 1)))))

# Increase the maximum line width for the Z3 Python formula pretty printer
set_option(max_width=120)
print Relations

# Encoding of the conjecture
# ((forall i:[1,m].func2(p,i)==Z)&&(q==func1(p))) implies (forall i:[1,m-1].func2(q,i)==Z)
Conjecture = Implies(And(q == func1(p), ForAll([i], Implies(And(1 <= i, i <= m), func2(p, i) == Z))),
                     ForAll([i], Implies(And(1 <= i, i <= m - 1), func2(q, i) == Z)))
print Conjecture

prove(Implies(Relations, Conjecture))
于 2013-01-06T17:29:29.280 に答える