如何在SMTLIB/Z3/CVC4中声明全称量词forall并编写受限量化断言

SMT-LIB2语法没有内置的“带范围约束的量化”简写形式，所有对变量取值的限制，都需要显式整合到量化的主体逻辑中，不存在在绑定变量阶段直接写范围判断的语法支持。
要实现forall x < 100, f(x) = 100这类受限量化的语义，核心是通过蕴含关系把范围约束和目标校验逻辑绑定，对应可直接使用的断言写法如下：

(assert
    (forall ((x Int))
        (=>
            (< x 100)  ; x的取值范围约束
            (= (incUntil100 x) 100)  ; 待校验的函数属性
        )
    )
)

• 语义说明：上述写法完全等价于“对所有小于100的整数x，incUntil100(x)的返回值为100”，不存在语义偏差
• 常见错误提醒：切勿省略蕴含前件直接书写(forall ((x Int)) (= (incUntil100 x) 100))，这类写法的实际语义是“对全体整数x，incUntil100(x)都等于100”，不仅和你需要的范围约束不符，还会因为传入大于100的x时触发函数无限递归，导致求解器无法完成正常验证

• 你定义的incUntil100仅在x ≤ 100的输入下具备递归终止性：当x大于100时，逻辑会持续执行+1操作，永远无法走到x=100的返回分支，量化断言里的范围约束同时也承担了避免求解器进入无限递归推导的保护作用
• 求解效率优化：如果求解过程中出现耗时过长的问题，可以手动为量化逻辑指定匹配模式，引导求解器优先匹配incUntil100 x的函数实例，减少无意义的实例展开开销

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