[z3] Programming Z3

본 포스트는 Programming Z3를 읽고 정리한 내용입니다.

링크 : http://theory.stanford.edu/~nikolaj/programmingz3.html

 

1. Introduction

Z3는 background theories를 해결하기 위한 specialized 알고리즘들을 갖춘 SMT solver

  * SMT(Satisfiability Modulo Theories) : SMT problem은 고전적인 1차 논리로 표현되는 background theories(arithmetic, bit-vectors, arrays 등)의 조합과 관련된 logical formulas에 대한 decision problem

    SMT는 constraint satisfaction problem의 한 형태로 생각할 수 있으므로, constraint programming에 대한 공식화된 접근 방식

  출처 : https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

 

Tutorial의 목적

  1) Z3의 available한 feature는? 어떤 용도로 설계됐는가?

  2) Z3에서 사용되는 underlying 알고리즘은 무엇인가?

  3) Top of Z3에서 어떻게 어플리케이션을 프로그래밍할 수 있는가?

 

Z3 System Architecture

System Architecture of Z3, version 4.8

Z3는 2가지 interface를 제공

  SMT-LIB2 : 텍스트 파일 또는 pipe로 제공되는 스크립트

  C : C-based API를 통한 호출

 

Architecture 내 기능

  Formulas : draw from symbols whose meaning are defined by a set of Theories

  Solvers : provide services for deciding satisfiability of formula

  Tactics : provide means for pre-processing simplification and creating sub-goals

  Optimization : services allow users to solve satisfiability modulo objective functions to maximize or minimize values

 

 

Sort : Z3에서의 type

In