저는 Python-API에서 Z3을 사용하고 있습니다. 아주 큰 선형 산술 제약 조건을 설정 중입니다.Z3 Python-API에서 푸시/팝 관련 문제
그러나 push/pop은 check()이 무한대로 작동하도록합니다.
push/pop을 사용하지 않는다면 아무 문제가 없습니다. 하지만 난 그냥 s.check() 전에 어딘가에
s.push()
s.pop()
를 삽입 할 때 s.check() 실행 끝없는 다음. pop없이 push 만 사용하면 정상적으로 작동합니다.
알려진 문제점 및 해결 방법이 있습니까? MacOS 10.7.5에서 Z3 [버전 4.3.1 - 64 비트]를 사용하고 있습니다.
덕분에 많은 & 안부, 클라우스
Z3는 솔버의 모음입니다. 그러나 그 중 하나만 증분됩니다. 비 증분 솔버는 문제에 훨씬 효율적입니다. s.push()을 사용할 때 Z3은 점진적으로 문제를 해결하고 "점진적 (범용)"솔버로 전환하려고합니다.
파일 시작 부분에 다음 명령을 추가하면 Z3에 여러 메시지가 표시됩니다. s.push()을 사용하면 메시지가 완전히 다릅니다.
set_option(verbose=10)
Z3에 특정 솔버를 사용하도록 할 수 있습니다. 예를 들어, 우리는 Z3는 s.push()를 사용하는 경우에도 효율적인 솔버를 사용합니다, 그리고
s = Tactic('qflia').solver()
와
s = Solver()
을 대체합니다. 그러나 처음부터 모든 check() 명령이 시작됩니다. 나는 비 증분과 증분 사이의 성능 차이가 매우 크기 때문에 이것이 문제의 문제라고 생각하지 않습니다.
친애하는 Leonardo, 감사합니다! qflia 전술은 저를 위해 잘 작동합니다. 그러나, 나는 내 코드에 's.reset()'을 가지고 있는데, 이것은 세분화 오류를 일으킨다 : 11 'resp. 'c.py (39) : 오류 : 예외 : 0x00000008을 읽는 액세스 위반' 나는 's.reset()'을 제거하고 이제는 작동합니다. qflia에 reset()이 허용되지 않습니까? 아니면 버그입니까? – Klaus
더 많은 질문;) 거기에 어떤 rise4fun 예제 어디에서 시간 제한을 설치하는 방법을 볼 수 있습니다 파이썬 API에서 s.check() 호출? 감사합니다 – Klaus
'Segfault'는'불안정한'(작업중인) 지점에서 수정되었습니다. 수정 프로그램은 야간 빌드에서도 사용할 수 있습니다 (http://research.microsoft.com/en-us/um/people/leonardo/blog/2013/02/15/precompiled.html). –
설명 된 동작을 보여주는 rise4fun-example에 대한 링크를 제공 할 수 있습니까? –
친애하는 말테, 여기에 예제를 찾을 수 있습니다 : http://rise4fun.com/Z3Py/UATh NUM_A 및 NUM_B에 대해 주어진 값으로, 나는 어떤 push() 및 Pop()도 사용하지 않을 때 문제를 해결합니다.). 그러나 23 번째 줄에 push()를 추가하면 타임 아웃이 발생합니다. 이 효과는 NUM_B = 3 대신 NUM_B = 10으로 훨씬 더 높습니다. 그러면 Z3py가 적절한 시간에 문제를 해결하지만 훨씬 긴 resp가 필요합니다. push()를 추가 할 때 끝이 없습니다. 나는 push() & pop()! 때문에 런타임이 그렇게 많이 다른 이유를 모르겠다. 감사합니다. 클라우스 추신. 파이썬 스크립트에서도 타임 아웃을 정의 할 수 있습니까? – Klaus