Z3求解器返回结果中的div0和mod0字段含义是什么？

Z3模型输出div0、mod0字段说明 #

你代码中使用了整数除法运算，Z3在求解时会将所有整数除法、取模的运算规则统一维护在特殊的映射变量中，这两个字段的具体含义如下：

• div0 是整数除法的运算映射表：
  你的代码中共出现3处整数除法：d/a、b/d、(a*c)/(b*d)，表中的条目就是这些除法的参数和对应结果：
  • (8, 4) -> 2 对应d/a = 8/4 = 2
  • (256, 64) -> 4 对应(a*c)/(b*d) = (4*64)/(8*8) = 256/64 =4
  • else -> 1 是兜底规则：所有未出现在上述列表中的整数除法输入组合，默认返回值为1，该值只要不违反你给出的约束条件即可，属于求解器自由设定的兜底值。
• mod0 是整数取模的运算映射表：
  你的代码中没有显式使用取模运算，因此只有兜底规则else -> 0，所有取模运算默认返回0，同样该兜底值不违反约束即可。

如果你的代码中没有用到整数除法、取模操作，Z3的模型输出就不会出现这两个特殊字段。

内容的提问来源于stack exchange，提问作者Simd