z3 C++ 인터페이스를 통해 SMT2 파일을 해석기로 읽을 수 있습니까?

Question

큰 시스템에 포함 된 z3 코드가 상당히 긴 시간 제한에도 불구하고 특정 제약 조건 세트 (C++ 인터페이스를 통해 추가 된)에 대한 솔루션을 찾지 못하는 문제가 있습니다. 구속 조건을 파일에 덤프 할 때 (솔버에서 check()) 호출 직전에 to_smt2() 메서드를 사용하고 독립 실행 형 z3 실행 파일을 통해 파일을 실행하면 약 4 초 내에 시스템을 해결합니다 (sat). 가치가있는 파일의 길이는 476,587 줄이므로 매우 큰 제약이 있습니다.

기존의 제약 조건을 대체하고 C++ 인터페이스를 사용하여 임베디드 솔버로 다시 읽어 들일 수있는 방법이 있습니까? 임베디드 버전이 독립 실행 형 솔버와 완전히 동일한 시작점에서부터 해결 될 수 있는지 확인하려면 어떻게해야합니까? (본질적으로 솔버 클래스에서 상응하는 from_smt2 (stream) 메쏘드를 어떻게 만들 수 있습니까?)

그들은 지금 당장과 같은 제약 조건을 가져야합니다. 그러나 그것들을 읽을 때 어떤 순서 효과가 계속 될 수 있습니다. 또는 우리가 그것을 포함 할 때 도입 된 솔버 또는 to_smt2()로 작성되지 않은 것에서 미묘한 차이가있을 수 있습니다. 그래서 가능한 경우 파일을 다시 읽어보고 차이점의 가능한 원인을 줄이려고합니다. 장기 실행 버전을 디버깅하는 동안 무엇을 찾아야하는지에 대한 제안이 도움이 될 것입니다.

기타 참고 사항 : 다른 사용자가 비슷한 문제가있는 것 같습니다 here. 그 사용자와는 달리, 제 문제는 모든 비트 벡터를 사용합니다. 유일한 알려지지 않은 결과는 임베디드 코드의 결과입니다. 임베디드 버전에 문제가있는 이유를 알아 내기 위해 C++ 인터페이스에서 (get-info : reason-unknown)을 호출하는 방법이 있나요?

Answer 1

검색 실패에 대한 설명을 검색하려면 "solver :: reason_unknown()"메서드를 사용할 수 있습니다. 파일과 문자열을 단일 식으로 구문 분석하는 방법이 있습니다. 어설 션 세트의 경우 표현식은 연결입니다. 편의상 솔버 클래스에 직접 이러한 메서드를 추가하는 것이 좋습니다. 그것은 다음과 같습니다 당신이 해결사 클래스의 외부에서 작성한다면

void from_smt2_string(char const* smt2benchmark) { 
     expr fml = ctx().parse_string(smt2benchmark); 
     add(fml); 
    } 

그래서 당신이 필요합니다 :

 expr fml = solver.ctx().parse_string(smt2benchmark); 
     solver.add(fml);