z3 python API에서 Implies 및 if 부울 명령을 사용하는 방법

Question

if-then-else을 구현하는 방법 Z3 python API를 첫 번째 주문 수식의 일부로 사용 하시겠습니까? 예 :

s.add(F, H, (if then else)). 

이와 관련된 질문은 어떻게 "내포합니다"부울을 사용하거나 "만약"이 목적을 위해 Z3 파이썬 온라인 가이드에 주어진 명령?

Answer 1

을 사용하여 Z3 Python API로 인코딩 된 표현 if(A, B, C). 다른 예는 상술 한 실시 예에 대한

F, H, A, B, C = Bools('F H A B C') 
s = Solver() 
s.add(F, H, Implies(A, B)) 
print s 

링크는 "내포"를 사용하여 여기

F, H, A, B, C = Bools('F H A B C') 
s = Solver() 
s.add(F, H, If(A, B, C)) 
print s 

: 여기서 은 일례이며, http://rise4fun.com/Z3Py/4BFhttp://rise4fun.com/Z3Py/JEU