1
SMT2 표준 (또는 Z3 확장)은 API 호출 "check_assumptions"와 동일한 명령을 제공합니까? Josh Berdine에 따르면 푸시 - 팝 스코프보다 가드 리터럴 및 check_assumptions을 사용하는 것이 더 빠릅니다. 그러나, 나는 지금 stdio를 통해 Z3을 사용하고있다. 그리고 (check-assumoptions p)만을 사용하면 unsupported이 나온다.stdin/smt2를 통한 check_assumptions?
감사합니다. 실제로 SMT-LIB2 표준에 언급되지는 않았지만 현재는 Z3 만 대상으로합니다. –
참고 : -smtc 옵션을 사용하면 더 이상 사용되지 않는 파서를 사용할 수 있습니다 (SMT 2.0 표준과 호환되지 않음). 이 프런트 엔드는 이후 버전의 Z3에서 제거 될 예정입니다. 새 SMT 2.0 파서에서 미사용 코어 추출에 대한 자세한 내용은 http://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3을 참조하십시오. –
감사합니다. SMT 2.0을 준수하는 것이 물론 더 좋습니다. –