어떻게 z3py에서 코어 수를 설정합니까

Question

http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html에 따르면 .smt 파일을 사용하는 경우 z3 명령 줄에서 CC_NUM_THREADS = 4를 설정할 수 있습니다.

z3py api를 사용하는 경우 어떻게해야합니까?

Answer 1

표제어 공유를 지원하는 포트폴리오 해결사는 최신 버전의 Z3에 포함되어 있지 않습니다. 따라서이 매개 변수는 지원되지 않으며 각 매개 변수에 대해 여러 값을 허용하는 매개 변수 형식은 명령 행 또는 Python을 통해 지원되지 않습니다.

그렇긴하지만 파 또는 전술 인 여러 코어를 활용하는 방법은 여전히 ​​있습니다. 예를 들어 Z3 Strategy Tutorial (par 또는 or 검색)을 참조하십시오. 이 예는 SMT2 입력 언어를 통해 여러 가지 전술을 병렬로 실행하는 방법을 보여줍니다 (이 예에서는 다른 임의의 시드로). z3py에서는 ParOr function을 사용하여 이와 같은 병렬 전략을 생성합니다.