주입 기능을 지원하지 않는 z3에 대한 해결 방법

SHA (x)와 같은 z3에서 해시 함수를 나타내고 싶습니다. 몇 가지 조사를 한 후에 z3이 분사 성을 잘 지원하지 않기 때문에 제약 조건을 가질 수 없다는 것을 깨달았습니다. (그리고 이것은 충돌로 인해 엄격히 말해서 진실이 아니라는 것을 깨닫는 동안, 휴리스틱으로 유용합니다. 프로젝트)주입 기능을 지원하지 않는 z3에 대한 해결 방법

forall([x, y],Implies(SHA(x)==SHA(y), x==y))

솔버가 종료 될 것으로 예상하십시오.

내 질문에이 문제에 대한 알려진 최적의 해결 방법이 있습니까? 예를 들어 한정 기호를 사용하지 않고 x와 y의 모든 쌍에 Implies (SHA (x) == SHA (y), x == y) 제약 조건을 추가하면 문제가 해결됩니까? 우리는 폼의 인코딩을 사용하여 해석의 기능 용

출처

2017-09-26 dirtyfilthy

: f는 단사 경우 (X [X] inverse_f (F (X)) =)

그래서, 우리는 기능을 도입 할 수

FORALL 그런 f의 범위에서 부분 역함수를 실현합니다. 동등한 쌍을 가진 정량화 된 공리는 매우 일반적이어서 Z3이 그들을 찾고 대신 위에 공리를 추가합니다. f가 발생할 때마다 인스턴스화됩니다. 물론 비트 벡터를 사용하여 인코딩되는 SHA의 경우 해석되지 않은 함수를 도입하면 Z3이 순수 SAT 솔버를 사용하지 않는다는 의미입니다. 가장 좋은 경우에는 Ackerman 인코딩으로 되돌아가 원래 페어 와이즈 인코딩을 다시 도입합니다.

출처

2017-09-26 15:06:18

부분 역변환을 사용하면 여전히 Implies (f (x) == f (y), x == y)의 순진한 접근법을 사용하는 것과 똑같은 문제가 있습니다. 즉 해결자가 솔루션을 찾을 수 없습니다. 간단한 문제. 예 : '수입 Z3 z3.BitVec A = ('A ', 32) z3.BitVec B = ('B ', 32) z3.BitVec X = ('X ', 32)의 해시 (32), z3.BitVecSort (32)) hash_inv = z3.Function ('hash', z3.BitVecSort (32), z3.BitVecSort (32)) hash_preds = z3.Solver() z3.set_param (자세한 정보 = 10) s.add (hash_pred) s.add (해쉬 (x)) == x) a)! = hash (b)) s.add (a! = b) s.check()' – dirtyfilthy

주입 기능을 지원하지 않는 z3에 대한 해결 방법

답변

관련 문제