Constrained Horn clauses

带有一阶理论约束的 Horn Clause，形如：

$$\phi \wedge P_1(x)\wedge P_2(x)\dots \to P(x)$$

其中 $P_1,P_2,\dots P$ 是谓词符号。$P(x)$ 处 (Head) 也可以是约束 $\psi$

判定

约束为 linear integer arithmetic 的 CHC 可满足性不可判定

CHC 求解器

• Z3/Spacer
• SeaHorn
• …