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不支持注入的解决方法

回答

相关问题