z3py를 사용하여 가장 약한 전제 조건 찾기

Question

z3py를 사용하여 작업 및 사후 조건이 주어진 경우 가장 약한 전제 조건을 찾고 싶습니다.

는 가장 약한 전제 조건 N의 ==이 방법은 일부 게시물 조건이 아닌 다른 사람을 위해 작동하는 전술 solve-eqs 사용 4.

될 작업 N = N + 1 및 사후 조건 N == 5을 감안할 때. 게시 조건 N < 5을 사용할 때 [[Not(4 <= N)]]이 나옵니다.

N == 5을 사용하는 경우 [[]]이 나올 때 N == 4을 입력하십시오.

N2 = Int('N2') # N after the action 
N = Int('N') # N before the action 

weakestPreconditionGoal = Goal() 

# 'N2 == n + 1' action 
# 'N2 == 5' post condition. 
weakestPreconditionGoal.add(N2 == N + 1, N2 == 5) 

t = Tactic('solve-eqs') 
wp = t(weakestPreconditionGoal) 
print(wp) 

약한 전제 조건을 찾는 가장 좋은 방법입니까?

나는 여러 가지 방법을 시도했지만 Z3에 익숙하지 않으며 취할 접근법이나 구현 방법을 알 수 없습니다.

Answer 1

예, solve-eqs은 동등성을 제거하는 데 사용할 수 있습니다. 문제는 어떤 평등이 제거 될지에 대한 통제력이 없다는 것입니다. 또 다른 옵션은 qe (한정 기호 제거)을 사용하는 것입니다. 이 예제는 here에서도 사용할 수 있습니다.

N2 = Int('N2') # N after the action 
N = Int('N') # N before the action 

weakestPreconditionGoal = Goal() 

# 'N2 == n + 1' action 
# 'N2 == 5' post condition. 
weakestPreconditionGoal.add(Exists([N2], And(N2 == N + 1, N2 == 5))) 

t = Tactic('qe') 
wp = t(weakestPreconditionGoal) 
print(wp) 

또 다른 옵션은 solve-eqs을 사용하는 것입니다,하지만 우리는 제거하지 않으 "가드"방정식. 우리는 보조 술어 guard을 사용하여 방정식을 보호 할 수 있습니다. 다음은 예제입니다 (온라인 here에서도 사용 가능). 물론 결과에서 guard을 제거하기 위해 두 번째 패스를 수행해야합니다.

N2 = Int('N2') # N after the action 
N = Int('N') # N before the action 
guard = Function('guard', BoolSort(), BoolSort()) 

weakestPreconditionGoal = Goal() 

# 'N2 == n + 1' action 
# 'N2 == 5' post condition. 
weakestPreconditionGoal.add(N2 == N + 1, guard(N2 == 5)) 

t = Tactic('solve-eqs') 
wp = t(weakestPreconditionGoal) 
print(wp)