SMT 란 ?컴퓨터 과학 및 수학에서 SMT는 해당 mathematical formulation (수학적 공식)을 만족하는 지 결정하는 문제입니다. 기존의 Boolean satisfiability (SAT)는 Boolean formulation만 표현할 수 있지만, SMT는 추가적으로 실수, 정수, list, array, bit vector, 그리고 str과 같은 다양한 data를 사용한 보다 복합적인 formulation을 해결할 수 있습니다. 다음은 SAT의 예시입니다.$$(A\lor \neg B)\land (B \lor C)$$이 SAT 문제의 해결책은 A, B, C에 Boolean value를 할당하여, 표현식을 참으로 만드는 조합을 찾는 것입니다.예로 A=1, B=0, C=1이면 표현식은 참이 ..
