math - 在 z3 中定义一个庞大但已知的函数

Question

我想用 z3 来解决纯数学中的可满足性问题。求解器必须推理 sort 函数Function('mult', BitVecSort(8), BitVecSort(8), BitVecSort(8), BitVecSort(8), BitVecSort(8), BitVecSort(8), BitVecSort(8))。这个函数已经是完全已知的，所以理论上我们可以通过输入表单的所有约束来定义它

mult(0, 26, 1, 0, 78, 1) == 1,
mult(11, 5, 1, 149, 9, 2) == 4,
mult(23, 8, 1, 116, 11, 1) == 10, ...

但由于需要大量的约束，这是不可行的。

但是，只有 125,501 个输出值非常难以计算，而其他所有值一旦知道就很容易计算。我可以在 z3 中输入所有 125,501 个约束，求解器会在几分钟内构建模型（我使用了Tactic('bv').solver()）。

有一些通用语句适用于mult，例如 ForAll([s1,s2,f1,f2,v1,v2], mult(s1,f1,v1,s2,f2,v2) == mult(s2,f2,v2,s1,f1,v1))，但已经添加此约束需要花费不合理的长时间来检查（它现在已经运行了超过 24 小时）。

有没有更简单的方法可以在 z3 中导入我的函数？对于 z3 来说，它是否太大而无法有效地推理它？

标签： mathz3z3py