Python 문자열로 표현된 C structs와 Python Value 간의 변환

파일에 Binary Data를 저장하거나 Network Connection 시 사용

struct.pack(fmt, v1, v2,...)

- 지정된 Format에 따라 v1, v2의 value를 Pack을 수행하며 그 결과는 String으로 리턴

struct.unpack(fmt, string)

- 지정된 Format에 따라 String을 Unpack을 수행하며 그 결과는 Tuple로 리턴

CharacterByte orderSizeAlignment

@ native native native
= native standard none
< little-endian standard none
> big-endian standard none
! network (= big-endian) standard none

 

FormatC TypePython typeStandard sizeNotes

x pad byte no value    
c char string of length 1 1  
b signed char integer 1 (3)
B unsigned char integer 1 (3)
? _Bool bool 1 (1)
h short integer 2 (3)
H unsigned short integer 2 (3)
i int integer 4 (3)
I unsigned int integer 4 (3)
l long integer 4 (3)
L unsigned long integer 4 (3)
q long long integer 8 (2), (3)
Q unsigned long long integer 8 (2), (3)
f float float 4 (4)
d double float 8 (4)
s char[] string    
p char[] string    
P void * integer   (5), (3)

 

ex) struct.pack('<B',i)

'Python' 카테고리의 다른 글

python struct module  (0) 2019.11.21
파이썬 리스트의 문자열을 int 형태로 변환  (2) 2019.02.18
Python z3 모듈  (0) 2018.12.02

list_a = ['1', '2', '3', '4']   -> list_a = [1, 2, 3, 4] 로 바꾸고 싶을 때,

 

list_a = map(int, list_a)   를 해주면 된다.

 

or list_a = [int(i) for i in list_a]

 

'Python' 카테고리의 다른 글

python struct module  (0) 2019.11.21
파이썬 리스트의 문자열을 int 형태로 변환  (2) 2019.02.18
Python z3 모듈  (0) 2018.12.02
  1. 12 2019.11.14 16:22

    혹시 리스트가
    [['1','2','3'], ['4','5','6']] 인 경우에
    문자열을 int 형태로 어떻게 변환하나요?

    • Realsung 2019.11.17 13:17 신고

      a=[['1','2','3'], ['4','5','6']]
      b=[]
      for i in range(len(a)):
      for j in range(len(a[0])):
      b.append(int(a[i][j]))

Python z3 Module

더 추가할 예정!

z3에 대해 공부할겸 올려봅니다.. ㅎ 틀린부분이나 팁?그런거 있으면 알려주세요

모듈 링크 : https://github.com/Z3Prover/z3

유용한 외국 문서 : https://ericpony.github.io/z3py-tutorial/guide-examples.htm

일반적으로 그냥 근의 공식을 사용해서 프로그래밍을 해서 방정식의 근을 구하는 것은 imperative programming 방식이다.

파이썬의 z3 SMT solver 모듈을 사용해서 방정식의 근을 구하는 것은 decalarative programming이다.

나는 SMT solver 모듈을 사용하는 법에 대해 간단하게 공부하면서 포스팅하겠돠..

SMT solver?

Satisfiability Modulo Theories의 약자이다.

수식을 만족하는 값이 존재하는지 찾아준다. 수식을 만족하는 값이 존재할 경우 그 값을 구해준다.

True or False + 방정식, 부등식 해 구하기

Function

from z3 import *

z3 모듈 사용하기 위해 임포트

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

Int()는 미지수(정수)를 선언

x = Real('x')
y = Real('y')

Real()은 미지수(실수)를 선언

x = BitVec('x',8)
y = BitVec('y',8)

BitVec() 미지수(비트 벡터)를 선언

비트 연산을 할 때 사용되는데 BitVec('미지수',n)으로 n비트 미지수를 선언 해준다.

set_option(precision=3)

Real()을 사용했을 때 3자리 까지만 출력하고 싶다면 set_option 함수 사용

s = Solver()

Solver 객체 생성하는 함수

https://z3prover.github.io/api/html/classz3py_1_1_solver.html

위에 Solver()에 대해 많은 예제와 함수들이 있습니다.

s.add()

s.append() 

s.assert_exprs()

s.Insert()

수식을 추가하는 함수

s.assertions()

추가된 수식을 반환하는 함수

s.push()

s.pop()

수식을 넣고 빼는 함수

s.check()

값이 존재하면 sat 값이 존재하지 않으면 unsat을 반환

s.model()

값이 존재할 경우 값을 구해주는 함수

unsat , unknown이면 에러를 반환

s.reason_unknown()

check() 함수의 반환 값이 unknown인 이유를 알려줌

s.reset()

추가한 수식을 초기화 시키는 함수

Example

from z3 import *
x = Int('x')
s = Solver()
s.insert(x*x-4*x+3==0)
print s.check()
print s.model()

x^2 - 4x +3 =0을 풀어주는 예시다.

'Python' 카테고리의 다른 글

python struct module  (0) 2019.11.21
파이썬 리스트의 문자열을 int 형태로 변환  (2) 2019.02.18
Python z3 모듈  (0) 2018.12.02

+ Recent posts