z3不支持注入的解決方法

我想在z3中表示一個哈希函數，類似於SHA（x）。在做了一些研究之後，看起來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

對於我們使用的形式的編碼未解釋的功能：

FORALL（[X]，inverse_f（F（X））= X）

所以當f是單射，我們可以引入一個函數，它在f的範圍內實現了部分逆。量化的公理與平等配對是如此的普遍，以至於Z3尋找它們並增加上述公理。它被實例化爲f的每一次出現。當然，對於通常使用位向量編碼的SHA來說，引入一個未解釋的函數意味着Z3不使用純SAT求解器。最好的情況是恢復到Ackerman編碼，這只是重新引入了原始的成對編碼。

來源

2017-09-26 15:06:18

使用部分逆我仍然有使用Implies（f（x）== f（y），x == y）的樸素方法的問題，即求解器無法找到解決方案簡單的問題。例如： '進口Z3 一個= z3.BitVec（ '一個'，32） B = z3.BitVec（ 'B'，32） X = z3.BitVec（ 'X'，32）散列= z3.Function（'hash'，z3.BitVecSort（32），z3.BitVecSort（32）） hash_inv = z3.Function（'hash'，z3.BitVecSort（32），z3.BitVecSort（32）） hash_pred = z3.ForAll（[x]，hash_inv（hash（x））== x） s = z3.Solver（） z3.set_param（verbose = 10）s.add（hash_pred） s.add（hash a）！= hash（b）） s.add（a！= b） s.check（）' – dirtyfilthy

z3不支持注入的解決方法

回答

相關問題