해결기 교체의 기반
응용 도구가 특정 해결기의 자료형에만 의존하면 다른 해결기를 시험하기 어렵다. Smt-Switch는 해결기와 타입, 논리 항을 추상 클래스로 다룬다. 공통 API를 사용하더라도 각 해결기가 지원하는 논리와 기능까지 같아지는 것은 아니다.
논리식 형태를 보존하기
해결기는 식을 만드는 순간 단순화하거나 일부 타입을 동일하게 취급할 수 있다. LoggingSolver는 구성한 항의 연산과 자식 정보를 따로 추적해 API 수준의 형태를 보존한다. 내부 해결기의 단순화가 중단되는 것이 아니라 공통 계층에서 보이는 표현을 관리하는 방식이다.
빌드와 의존성
사용할 해결기는 빌드 구성에서 선택한다. 공통 라이브러리만 만들어졌다고 실제 해결기가 포함되었다고 볼 수 없다. 해결기별 지원 버전과 추가 의존성, 배포 조건을 확인해야 하며 결과를 비교할 때는 백엔드와 옵션을 함께 맞춘다.