맞춤 이론을 갖춘 SMT 솔버?

Question

기본 이론으로 정규 트리 문법을 사용하는 검증 작업을하고 있습니다.

Z3을 사용하면 해석되지 않은 함수로 자신 만의 내용을 정의 할 수 있지만 의사 결정 절차가 재귀적일 때는 언제나 잘 작동하지 않습니다. 그들은 플러그인을 허용하는 데 사용했지만 그것은 depricated되었습니다, 제 생각에는.

내가 궁금한 점은, 사용자 정의 이론을위한 의사 결정 절차를 작성할 수있는 적절한 SMT 솔버에 대한 권장 사항이 있습니까?

Answer 1

대부분의 합리적인 SMT 솔버가 오픈 소스이기 때문에 몇 가지 옵션이 있습니다. 이론적 인 솔버를 지출해야하는 시간과 에너지의 양에 따라 세부적으로 통합 할 수 있습니다.

• OpenSMT 은 플러그 가능한 이론 통합을 위해 특별히 제작되었습니다.
• VeriT, Yices 및 CVC4는 오픈 소스이므로이 솔버에서 이론 통합을 살펴볼 수 있습니다.
• Z3은 공개 소스이므로 나와 다른 사람들이 사용 가능하게 설정할 수 있습니다. DPLL (T) 플러그인 모드 용 API가 있지만 Z3 소스가 열리면 기본 제한 사항으로 인해 모델이 제거되었습니다. 모델 구성을 제대로 지원하지 않았습니다. 이론을 연결하는 데 사용되는 내부 API는 원칙적으로 외부 API와 동형입니다. 이론을 통합하는 다양한 방법을 설명하는 오래된 논문은 https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-aplas11.pdf입니다. 첫 번째 프로토 타입은 솔버 주위의 바깥 쪽 루프를 사용하면 훨씬 쉽게 구현할 수 있다고합니다. 솔버로부터 명제 모델을 얻은 다음 그것이 당신의 배경 이론을 만족시키는 지 확인하십시오. 내부 API를 사용해 볼 수도 있습니다. 이론에 따라서는 상당히 쉽습니다. 예를 들어 UTVPI https://github.com/Z3Prover/z3/blob/master/src/smt/theory_utvpi_def.h을 샘플로보십시오. 문자열 이론에 대해서는 상당히 관련이 있습니다 (이론에 상당한 특수한 경우 추론이 필요하기 때문에). z3str3 모듈은 올해 초에 통합되었으며 https://github.com/Z3Prover/z3/blob/master/src/smt/theory_str.cpp이며 개발이 아직 진행 중입니다. 약 10KLOC입니다. Bui Phi Dep는 외부 이론 통합 https://github.com/diepbp/FAT에 Z3의 이전 버전을 사용합니다. 문자열과 트랜스 듀서 이론이 꽤 많은 설정을 필요로 할 때 이것은 또한 상당한 양의 코드입니다. 사용자 버그 보고서 및 요청에 기꺼이 응대하는 기고가에게 우리는 (Z3) Z3의 주요 지부에 적용되지 않는 이론 및 알고리즘을 추가로 제공 할 것을 매우 환영합니다. 문자열과 트리 수락 자/변환기 공간에는 약간의 흔들림이 있습니다.

다시 말하지만, 첫 번째 버전에서는 SMT 솔버가 명제 SAT 및 해석되지 않은 함수 (및 필요한 경우 산술)를 처리하도록하는 외부 통합을 통해 상당히 멀리 떨어져 있어야합니다. 그런 다음 솔버에서 모델을 요청하고 솔버로부터 얻은 propositional 모델이 이론과 일치 할 때까지 이론 공리를 다시 추가 할 수 있습니다 (또는 UNSAT을 얻음). 명제 모델의 모든 과제가 관련성이있는 것은 아닙니다. 이중 전파 (http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD14/proceedings/29_niemetz.pdf)를 적용하여 고려한 할당 수를 최소화 할 수 있습니다.