SMT-LIB 2.6 선언 데이터 형식 문의 SMT 솔버 지원

SMT-LIB 버전 2.6의 draft은 (declare-datatypes) 문을 지정합니다. 이 기능의 경우 original announcement에서 제안 된 구문은 당시 Z3 및 CVC4에서 지원하는 구문과 다릅니다.SMT-LIB 2.6 선언 데이터 형식 문의 SMT 솔버 지원

현재 SMT-LIB 2.6 초안의 제안 구문을 지원하는 SMT-LIB 지원이있는 SMT 해석기 또는 제안 된 구문에 대한 지원을 해석기에 추가하는 패치가 있습니까?

관심있는 논리는 QF_ABV와 간단한 n 튜플에 대한 데이터 유형입니다. 재귀 데이터 유형이나 매개 변수 데이터 유형과 같은 고급 데이터 유형 기능은 필요하지 않습니다.

출처

2017-03-13 CliffordVienna

Z3 아직의 구문을 구현하지 않습니다 사양 초안. 보다 실질적인 변화는 패턴 매칭 컴파일러를 사용하여 컴파일 될 수있는 패턴 매칭 (또는 LISP 프로그래머가 손으로 할 수있는 것처럼)의 도입이다. –

CVT4 (커밋 594301e6f2893ebe9baba5083ff084933b1e9da9)의 최신 개발 버전에서 SMT LIB 버전 2.6 데이터 유형에 대한 지원이 추가되었습니다. 2.6 구문은 기본적으로 사용되지 않습니다,하지만 당신은 사용할 수 있습니다

cvc4 --lang = smt2.6 [입력]이 도움이

희망, 앤드류

출처

2017-03-16 18:32:37 user7723234

고마워요! JFYI : Yosys의 write_smt2 명령 (따라서 yosys-smtbmc)은 이제 SMT-LIB 2.6 데이터 유형을 사용할 수 있습니다. 다음은 예제입니다. http://scratch.clifford.at/datatypedemo.smt2 – CliffordVienna

SMT-LIB 2.6 선언 데이터 형식 문의 SMT 솔버 지원

답변

관련 문제