Z3 : 수식 연산이 구체적인 값을 반환하는지 Z3에서 알 수 있습니까? 우리는 쉽게 그 (C - B) 볼 수 있습니다</p> <pre><code>a, b, c = BitVecs('a b c', 32) a == b + c c == b + 5 </code></pre> <p>구체적인 값을 반환합니다 (숫자 5), 그러나 (a는 - B) - B 추상적 뭔가 (A 때문에를 반환

Z3은 정리 해설자이지만 제약 해법으로도 볼 수 있습니다. a == b + c과 같은 표현식을 제약 조건으로 볼 수 있습니다. Z3 Python 인터페이스에는 solve이라는 명령이 있습니다. 제약 조건을 풀려고 시도합니다. 즉, 모든 제약 조건을 충족시키는 "할당"을 찾으려고합니다. 예를 들어 다음 명령을 실행하면 (here도 가능)

[b = 0, a = 5, c = 5]

우리는 해결책 "만족"제약 말 :

a, b, c = BitVecs('a b c', 32) 
solve(a == b + c, c == b + 5)

그것은 솔루션을 생산하고 있습니다. Z3에는 몇 가지 다른 명령과 API가 있습니다. 을 참조하십시오.

출처

2013-04-15 03:21:52

레오, 감사합니다. 실제로 내가 원했던 것은 c가 항상 5의 동일한 구체적인 값을 갖는지 확인하는 것입니다. 간단한 솔루션을 생각해 냈습니다 : c의 모델을 찾은 다음 다른 구속 조건 (예 : c! = 5)을 추가하여 갈등이있다. 있을 경우, c는 항상 상수 값 5를 갖습니다. – user311703

예, 이것이 그것을 수행하는 방법입니다. –

다른 질문 : "반대"제약 조건을 자동 생성하기 위해 Z3을 어떻게 사용할 수 있습니까? 예를 들어, "c == 5"의 반대는 "c! = 5"또는 "a> b"의 반대는 "a <= b"입니다. 이것이 가능하다면 "반대"제약 조건을 생성하는 방법은 무엇입니까? (나는 여기서 "반대"용어를 발명했다. 문학에서 그들이 무엇을 부르는 지 알지 못한다.) – user311703

답변

관련 문제