如何用SMT工具证明含模运算的等式？求解无返回问题排查

问题背景 #

需证明或推翻以下等式：

((pid+1)%NP + i)%NP = (pid + i + 1)%NP

已知条件：pid、i、NP均为整数，且满足 0≤pid<NP、0≤i。推测等式成立，但使用CVC5、Z3等SMT工具运行编写的SMT2代码时，工具无返回结果。

使用的SMT2代码如下：

(declare-const i Int)
(declare-const pid Int)
(declare-const NP Int)
(assert (<= 0 pid))
(assert (< pid NP))
(assert (<= 0 i))
(assert (not
  (= (mod (+ (mod (+ pid 1) NP) i) NP)
     (mod (+ pid i 1) NP))))
(check-sat)

解决提示 #

• 补充NP的正整数约束：原代码未限制NP为正整数，但根据0≤pid<NP的条件，NP必须是大于0的整数。SMT工具在处理NP≤0的情况时，模运算的语义会出现歧义（如除数为0或负数），导致工具陷入无意义的搜索无法终止。需添加约束：

  (assert (> NP 0))
  

  添加后再运行，工具会返回unsat，证明等式成立。
• 验证工具模运算语义：不同SMT工具对整数模运算的定义可能存在差异，但在NP>0的约束下，主流工具（Z3、CVC5）的模运算结果均为非负整数，符合数学上的模运算定义，此时等式的等价性可被工具正确验证。
• 分步测试简化问题：若仍有疑问，可先固定NP为具体正整数（如(assert (= NP 5))），运行代码验证等式在特定值下成立，再推广到全域情况，帮助定位问题。

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