3
내 연구에서는 자동으로 SMT2를 생성 한 다음 Z3으로 전달합니다. 생성 된 코드는 기본적으로 하나의 매우 큰 연결 (and ...) 많은 제약이 있습니다. 많은 어설 션을 생성하는 것과는 대조적으로,이를 수행하여 중요한 성능을 잃게됩니까?Z3 성능 : 많은 어설 션 대 대형 연결
A
답변
3
당신은 잃거나 얻지 않을 것입니다. 거의 모든 설정에서 Z3은 모든 연결을 여러 개의 어설 션으로 나눕니다. 그렇게하기까지 걸리는 시간은 거의 없습니다. Which is better practice in SMT: to add multiple assertions or single and?
나는 당신이 당신의 제약에 속하는 이론에 대한 세부 사항을 제공하지 않는 것이 주어진 질문에 대한 명확한 답을하지 않을 것이라는 말을 감히 :
이 질문도하기 전에왔다. 그리고 그랬더라도, 만족 스러움을주는 것은 여전히 어려울 것입니다. 실험을 먼저 실행하고 (두 가지 모양 모두 생성), 필요하다면 여기로 돌아와 결과에 대해보고하고 그 결과를 바탕으로 질문을 수정하십시오. –