1
고정 점을 지원하는 Z3 이외의 smt 도구가 있습니까?고정 점을 지원하는 SMT 도구
A
답변
4
고정 점에 의해, 나는 혼의 절 쿼리에 대한 해결을 의미한다고 가정합니다. 유사한 성격의 문제를 해결하는 도구가 많이 있지만 정확히 같은 형식이 아닐 수도 있습니다. Philippe Suter's Leon tool은 다른 알고리즘을 사용하며 재귀 적 프로그램보다 많은 정확성 쿼리를 해결할 수 있습니다. 안드레이 리발 첸코 (Andrey Rybalchenko)의 ARMC 도구는 선형 실제 연산을 사용하여 호른 수식을 해결합니다. 또한 종료 조건을 설정할 수 있습니다. 테이블 링이있는 CLP 시스템은 Z3과 유사한 형식으로 쿼리를 해결할 수 있어야합니다 (둘 다 혼 포맷을 입력 포맷으로 사용). 또한 문맥에 따라 사용할 수있는 많은 기호 모델 검사 솔버가 있습니다.