Z3Py 튜 토리 얼 (번역)

원문:https://ericpony.github.io/z3py-tutorial/guide-examples.htm
연습:http://3xp10it.cc/auxilary/2017/11/14/z3-solver%E5%AD%A6%E4%B9%A0/
주: 이 번역 은 스스로 즐 기 는 데 쓰 인 다.
Python 에서 Z3 API 사용 하기
z3 는 Microsoft Research 가 개발 한 고성능 의 정리 증명 도구 이다.z3 는 소프트웨어 / 하드웨어 의 검증 과 테스트, 제약 문제 해결, 혼합 시스템 분석, 안전 분야, 생물학 과 기하학 적 문제 등 여러 응용 에 자주 사용 된다.
이 튜 토리 얼 은 z3py 의 주요 기능, 즉 python 에서 z3 api 를 사용 하 는 것 을 보 여 줍 니 다. 꼭 따라 실험 하 십시오.
 
시작 하 다
우 리 는 간단 한 예 를 보 자.

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

Int ('x') 함수 가 z3 의 성형 변 수 를 x 라 고 만 들 었 고 solve 함수 가 제약 시스템 을 풀 었 습 니 다. 이 예 는 두 개의 변수 x 와 y, 그리고 세 개의 제약 조건 을 사 용 했 습 니 다.z3py 는 python 과 마찬가지 로 "=" 을 사용 하여 값 을 부여 합 니 다. 사용, > =, = =,! =비교 해 보 겠 습 니 다.상기 예 에서 표현 식 'x + 2 * y = = 7' 은 z3 제약 조건 입 니 다.
기본적으로 z3py 는 공식 이나 표현 식 을 표시 할 때 수학의 표기 법 을 사용 합 니 다. 보통 ∧ 로 논리 기호 와, ∨ 로 논리 기호 나, 등등 을 표시 합 니 다.명령 setoption (html mode = True / False) 은 표현 식 의 형식 을 설정 할 수 있 습 니 다. True 는 수학 표기 법 을 사용 하고 False 는 z3py 표기 법 을 사용 합 니 다. 이것 도 오프라인 z3py 의 기본 모드 입 니 다.

x = Int('x')
y = Int('y')
print x**2 + y**2 >= 1
set_option(html_mode=False)
print x**2 + y**2 >= 1

z3 표현 식 내용 을 옮 겨 다 니 는 함 수 를 제공 합 니 다.

x = Int('x')
y = Int('y')
n = x + y >= 3
print "num args: ", n.num_args()
print "children: ", n.children()
print "1st child:", n.arg(0)
print "2nd child:", n.arg(1)
print "operator: ", n.decl()
print "op name:  ", n.decl().name() #  str

z3 모든 기본 적 인 수학 연산 자 를 제공 합 니 다.z3py 는 python 과 같은 연산 우선 순 위 를 사용 합 니 다.python 과 마찬가지 로 * * 는 멱 연산 을 대표 합 니 다.z3 는 비 선형 다항식 조건 의 제약 을 풀 수 있다.

x = Real('x')
y = Real('y')
solve(x**2 + y**2 > 3, x**3 + y < 5)

프로 세 스 Real ('x') 에서 실수 변수 x 를 만 들 었 습 니 다.z3py 는 임의의 큰 정수, 유리수 와 무 리 를 나 타 낼 수 있다.하나의 무리 수 는 정수 계수 다항식 의 뿌리 이다.내부 에서 z3py 는 이러한 수 를 정확하게 표시 하고 무리수 는 10 진법 소수 로 표시 하여 결 과 를 읽 기 에 편리 합 니 다.
 

x = Real('x')
y = Real('y')
solve(x**2 + y**2 == 3, x**3 == 2)

set_option(precision=30)
print "Solving, and displaying result with 30 decimal places"
solve(x**2 + y**2 == 3, x**3 == 2)

프로 세 스 setoption 은 z3 의 실행 환경 을 설정 하 는 데 사 용 됩 니 다.결 과 를 어떤 방식 으로 표시 할 지 전역 설정 옵션 을 설정 하 는 데 사 용 됩 니 다. precision = 30 을 선택 하고 10 진 디 스 플레이 결과 의 소수 자릿수 를 설정 합 니 다.1.2599210498?적중 하 다표지 출력 이 차단 되 었 습 니 다.
다음 예 는 흔히 볼 수 있 는 오 류 를 보 여 줍 니 다. 표현 식 1 / 3 은 하나의 python 성형 숫자 이지 z3 유리수 가 아 닙 니 다. 이 예 는 z3py 를 사용 하여 유리수 를 만 드 는 다른 방식 을 보 여 줍 니 다.프로 세 스 Q (num, den) 는 z3 유리 수 를 만 들 었 습 니 다. 이 유리 수 는 num 을 분자 로 하고 den 을 분모 로 합 니 다.프로 세 스 RealVal (1) 은 숫자 1 을 나타 내 는 z3 실 수 를 만 들 었 습 니 다.

print 1/3
print RealVal(1)/3
print Q(1,3)

x = Real('x')
print x + 1/3
print x + Q(1,3)
print x + "1/3"
print x + 0.25

유리수

x = Real('x')
solve(3*x == 1)

set_option(rational_to_decimal=True)
solve(3*x == 1)

set_option(precision=30)
solve(3*x == 1)

하나의 구속 시스템 이 풀 리 지 않 을 수도 있다. 이런 상황 에서 우 리 는 이 시스템 을 만족 시 킬 수 없 는 것 이 라 고 부른다.

x = Real('x')
solve(x > 4, x < 0)

python 과 마찬가지 로 주석 은 \ # 로 시작 하여 줄 바 꿈 문자 로 끝 납 니 다. z3py 는 여러 줄 의 주석 을 지원 하지 않 습 니 다.
BooLean Logic
z3 지원 불 연산 자: And, Or, Not, Implies, If.등가 사용

                    
p = Bool('p')
q = Bool('q')
r = Bool('r')
solve(Implies(p, q), r == Not(q), Or(Not(p), r))

python    True False    z3      
p = Bool('p')
q = Bool('q')
print And(p, q, True)
print simplify(And(p, q, True))
print simplify(And(p, False))


               
p = Bool('p')
x = Real('x')
solve(Or(x < 5, x > 10), Or(p, x**2 == 2), Not(p))

구 해기
z3 는 서로 다른 구 해 기 를 제공 했다.명령 solve 는 이전에 사용 되 었 습 니 다. z3 구문 API 를 사용 하여 이 루어 졌 습 니 다.그것 의 실현 은 z3 발행 판 의 z3. py 파일 에서 찾 을 수 있 습 니 다.다음 예 는 기본 Solver API 를 보 여 줍 니 다.

x = Int('x')
y = Int('y')

s = Solver()
print s

s.add(x > 10, y == x + 2)
print s
print "Solving constraints in the solver s ..."
print s.check()

print "Create a new scope..."
s.push()
s.add(y < 11)
print s
print "Solving updated set of constraints..."
print s.check()

print "Restoring state..."
s.pop()
print s
print "Solving restored set of constraints..."
print s.check()

솔 버 () 에 게 일반적인 구 해 기 를 만 들 라 고 명령 했다.제약 조건 은 방법 add 로 추가 할 수 있 습 니 다.우 리 는 이 구속 조건 이 이미 구 해기 에서 단언 되 었 다 고 말 했다.check () 방법 은 이러한 구속 조건 을 단언 하고 결과 sat 로 돌아 가 는 것 은 해 가 있 음 을 나타 내 며, unsat 는 해 가 없 음 을 나타 낸다.우리 도 이 시스템 이 단언 하 는 구속 조건 은 불가능 하 다 고 말 할 수 있다.마지막 으로 구 해 기 는 특정한 제약 시스템 을 풀 지 못 하고 알 수 없 는 결 과 를 되 돌려 줄 수도 있다.
일부 응용 프로그램 에서 우 리 는 제약 조건 을 공유 하 는 유사 한 문 제 를 탐구 하고 자 한다. 우 리 는 명령 push 와 POP 를 사용 하여 이 일 을 완성 할 수 있다.모든 풀이 기 는 단언 스 택 을 유지 합 니 다. push 에 게 현재 스 택 크기 를 저장 하 라 고 명령 합 니 다. pop 에 push 명령 과 일치 하 는 모든 단언 을 삭제 하 라 고 명령 합 니 다. check 방법 으로 작 동 하 는 대상 은 항상 현재 단언 스 택 에 있 습 니 다.
다음은 z3 가 풀 수 없 는 예 를 보 여 줍 니 다. s. check () 은 이러한 상황 에서 unknown 으로 돌아 갑 니 다.돌 이 켜 보면 Z3 는 비 선형 다항식 제약 을 해결 할 수 있 지만 2 * * x 는 다항식 이 아니다.

x = Real('x')
s = Solver()
s.add(2**x == 3)
print s.check()

다음 예제 에 서 는 구 해 기의 제약 조건 을 어떻게 옮 겨 다 니 는 지, check 방법의 성능 통계 정 보 를 어떻게 수집 하 는 지 보 여 줍 니 다.

x = Real('x')
y = Real('y')
s = Solver()
s.add(x > 1, y > 1, Or(x + y > 3, x - y < 2))
print "asserted constraints..."
for c in s.assertions():
    print c

print s.check()
print "statistics for the last check method..."
print s.statistics()
# Traversing statistics
for k, v in s.statistics():
    print "%s : %s" % (k, v)

z3 에서 단언 의 제약 조건 의 해 제 를 찾 았 을 때 check 명령 은 sat 로 돌아 갑 니 다.우 리 는 z3 가 일련의 제약 조건 을 만족 시 켰 고 이 를 하나의 모델 (model) 이 라 고 부 르 며 이 모델 은 단언 의 제약 조건 을 만족 시 켰 다.모델 은 모든 단언 의 구속 을 성립 시 키 는 해석 이다.다음 예 는 검사 모델 의 기본 방법 을 보 여 준다.

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
print s.check()

m = s.model()
print "x = %s" % m[x]

print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])
      ，  Reals('x y, z')   x，y，z，3   。          
x = Real('x')
y = Real('y')
z = Real('z')

표현 식 m [x] 는 x 가 모델 m 에서 설명 한 것 을 되 돌려 줍 니 다. 표현 식 '% s =% s'% (d. name (), m [d]) 는 문자열 을 되 돌려 줍 니 다. 그 중에서 첫 번 째% s 는 d. name () 으로 대체 되 고 두 번 째% s 는 m [d] 로 대체 되 며 필요 할 때 z3py 는 자동 으로 z3 대상 을 텍스트 표 현 형식 으로 변환 합 니 다.
 
계산 하 다
z3 는 실수 와 정수 변 수 를 지원 합 니 다. 어떤 문제 에서 혼합 하여 사용 할 수 있 습 니 다.대부분의 프로그램 언어 와 마찬가지 로 z3py 는 필요 할 때 성형 표현 식 을 실수 표현 식 으로 자동 으로 변환 합 니 다.다음 예 는 성형 변수 와 실수 변 수 를 서로 다른 방법 으로 설명 하 는 것 을 보 여 준다.

a, b, c = Ints('a b c')
d, e = Reals('d e')
solve(a > b + 2,
      a == 2*c + 10,
      c + b <= 1000,
      d >= e)
  simplify   z3        。
x, y = Reals('x y')
# Put expression in sum-of-monomials form
t = simplify((x + y)**3, som=True)
print t
# Use power operator
t = simplify(t, mul_to_power=True)
print t

명령 helpsimplify () 에서 선택 할 수 있 는 모든 동작 을 출력 합 니 다.z3py 는 사용자 가 두 가지 스타일 로 옵션 을 작성 할 수 있 도록 합 니 다.z3 내부 옵션 이름 은 ":" 로 시작 하고 단어 사 이 는 "-" 로 나 뉜 다.이 옵션 들 은 z3py 에 도 사용 할 수 있 습 니 다.z3py 도 클래스 python 의 이름 을 지원 합 니 다. 이때 "-" 삭제 되 었 습 니 다. "-" 는 "" 로 바 뀌 었 습 니 다. 다음 예 는 이 두 가지 스타일 을 보 여 줍 니 다.

x, y = Reals('x y')
# Using Z3 native option names
print simplify(x == y + 2, ':arith-lhs', True)
# Using Z3Py option names
print simplify(x == y + 2, arith_lhs=True)

print "
All available options:"
help_simplify()

z3py 는 임의의 큰 숫자 를 지원 합 니 다.아래 의 예 는 어떻게 대수 로 기본 적 인 산수 연산 을 하 는 지 보 여 준다.z3py 는 대수 상의 무리수 만 지원 하고 대수 상의 무리수 는 여러 가지 제약 조건 의 해 를 나 타 낼 수 있 습 니 다.z3py 는 무리수 를 십 진법 소수 의 가 독성 이 강 한 형식 으로 바 꾸 고 무리수 의 내부 표현 형식 은 sexpr () 방법 으로 추출 할 수 있 으 며 수학 공식 형식 이나 lisp 언어 와 유사 한 표현 식 으로 z3 의 내부 표현 형식 을 보 여 줍 니 다.

x, y = Reals('x y')
solve(x + 10000000000000000000000 == y, y > 20000000000000000)

print Sqrt(2) + Sqrt(3)
print simplify(Sqrt(2) + Sqrt(3))
print simplify(Sqrt(2) + Sqrt(3)).sexpr()
# The sexpr() method is available for any Z3 expression
print (x + Sqrt(y) * 2).sexpr()

기계 연산
현대 CPU 와 주류 프로그램 언어 는 고정된 크기 의 비트 벡터 를 사용 하여 연산 한다.z3py 에 서 는 bit - Vector 를 사용 하여 기계 연산 을 실현 할 수 있 습 니 다.그것 은 무 기호 연산 과 유 기호 연산 의 정확 한 정 의 를 실현 했다.
다음 예 는 비트 벡터 변수 와 상수 를 만 드 는 방법 을 보 여 줍 니 다.함수 BitVec ('x', 16) 는 z3 의 비트 벡터 이름 을 x 로 만 들 었 습 니 다. 크기 는 16 비트 입 니 다.편 의 를 위해 z3py 에서 정수 상수 상수 상 수 는 비트 벡터 표현 식 을 만 드 는 데 사용 할 수 있 습 니 다.함수 BitVecVal (10, 32) 은 크기 가 32 비트 인 비트 벡터 를 만 들 었 습 니 다. 그 수 치 는 10 입 니 다.

x = BitVec('x', 16)
y = BitVec('y', 16)
print x + 2
# Internal representation
print (x + 2).sexpr()

# -1 is equal to 65535 for 16-bit integers 
print simplify(x + y - 1)

# Creating bit-vector constants
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print simplify(a == b)

a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
# -1 is not equal to 65535 for 32-bit integers 
print simplify(a == b)

일부 프로그램 언어, 예 를 들 어 C, C + +, C \ #, 자바 등 은 기호 정수 와 기호 가 없 는 정수 가 위치 벡터 차원 에서 아무런 차이 가 없다.그러나 z3 는 기호 수 와 무 기호 수 에 서로 다른 연산 조작 버 전 을 제공 했다.z3py 에서 연산 자 는 > =, /,% 와 > > 기호 가 있 는 숫자 에 사용 되 며 기호 가 없 는 연산 자 는 ULT 입 니 다. ULE, UGT, UGE, UDiv, URem 화해시키다 LShR。

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)

solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)

solve(x < 0)

# using unsigned version of < 
solve(ULT(x, 0))

연산 자 > > 는 연산 자 오른쪽 이동 작업 이 고 <
 
함수.
(번역 이 안 돼)
프로그램 언어의 함수 에서 의외 의 상황 이 발생 할 수 있 습 니 다. 예 를 들 어 이상 하 게 던 지 거나 돌아 오지 않 습 니 다. 이 프로그램 언어 와 달리 z3 의 함수 에 서 는 이러한 상황 이 발생 하지 않 습 니 다. 이것 은 모든 입력 값 이 정의 되 었 기 때 문 입 니 다.z3 는 1 단계 논리 위 에 세 워 진 것 이다.
하나의 제약 조건, 예 를 들 어 x + y > 3 에 대해 우 리 는 x, y 는 모두 변수 라 고 할 수 있다. 일부 교재 에서 x 와 y 는 해석 되 지 않 은 양 이 라 고 불 린 다. 즉, 이 제약 조건 의 정확 한 해석 을 보장 하 는 모든 것 이 허용 된다 는 것 이다.
더욱 정확 한 것 은 함수 와 상수 기 호 는 1 단계 논리 에서 해석 되 지 않 거나 자유 로 운 것 이 라 고 할 수 있다. 즉, 선천적 인 해석 이 그들 에 게 부여 되 지 않 았 다.이것 은 서명 이론 에 속 하 는 함수 와 대 비 를 이룬다. 예 를 들 어 + 연산 은 고정 적 이 고 표준적 인 해석 을 가지 고 있 는데 바로 두 개의 수 를 더 하 는 것 이다.이런 자유로운 함수 와 상수 가 가장 큰 유연성 을 가지 고 있다.그들 은 제약 조건 을 만족 시 키 는 어떤 해석 도 허용 한다.
설명 되 지 않 은 함수 와 상수 를 설명 하기 위해 설명 되 지 않 은 정수 x, y 를 사용 하고 마지막 으로 f 를 설명 되 지 않 은 함수 로 하여 금 성형 파 라 메 터 를 받 아들 이 고 성형 값 을 되 돌려 줍 니 다.아래 의 예 는 어떻게 강제로 하나의 해석 이 나타 나 는 지 설명 하 였 다.

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
solve(f(f(x)) == x, f(x) == y, x != y)

 f    ：f(0) 1，f(1) 0，f(c) 1，  c  0 1    
 z3 ，                   。           evaluate  
x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
print s.check()
m = s.model()
print "f(f(x)) =", m.evaluate(f(f(x)))
print "f(x)    =", m.evaluate(f(x))

 
Satisfiability and Validity
설명 되 지 않 은 기호 에 대해 적당 한 할당 을 하면 방정식 이나 제약 조건 의 결 과 를 항상 true 로 만 들 수 있 고 방정식 이나 제약 조건 F 가 유효 하 다 고 한다.제약 조건 의 결 과 는 항상 true 를 조건 으로 하고 설명 되 지 않 은 기호 에 대한 적당 한 할당 이 존재 하면 제약 조건 으로 만족 할 수 있 습 니 다.유효성 은 명 제 를 찾 는 것 에 대한 증명 이 고 만족 성 은 제약 조건 을 찾 는 것 이다.방정식 F 가 a 와 b 를 포함 하 는 것 을 구상 합 니 다. 우 리 는 F 가 효과 가 있 는 지 물 었 을 때, 즉 임의의 값 의 a 와 b 에 게 그것 이 항상 true 인지 물 었 습 니 다.F 가 항상 true 이면 Not (F) 는 항상 false 입 니 다. 이때 a 와 b 는 만족 할 수 있 는 할당 조합 이 없 기 때문에 Not (F) 는 만족 할 수 없 기 때문에 이렇게 말 할 수 있 습 니 다. Not (F) 가 만족 할 수 없 을 때 F 는 유효 합 니 다.비슷 한 것 은 Not (F) 가 무효 일 때 F 는 만족 할 수 있 습 니 다.(주: 유효성 은 검증 을 통 해 판단 된다. 즉, 주어진 수 치 를 판단 하 는 것 이다. 임 의 판단 이 모두 무효 라면 만족 할 수 없다 고 한다. 명제 형식: 임 의 검증, 결과 가 모두 무효 라면 조건 제약 이 만족 할 수 없다 고 한다. 역 부: 조건 제약 이 만족 할 수 있다 면 검증 이 존재 하여 결 과 를 유효 하 게 한다)

p, q = Bools('p q')
demorgan = And(p, q) == Not(Or(Not(p), Not(q)))
print demorgan

def prove(f):
    s = Solver()
    s.add(Not(f))
    if s.check() == unsat:
        print "proved"
    else:
        print "failed to prove"

print "Proving demorgan..."
prove(demorgan)