我在以下看似微不足道的基准测试中尝试了几个SMT求解器(CVC3,CVC4和Z3):
(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)
所有的解决方案都归不为人知.我知道这是一个不可判断的片段(非线性),但我期待有一些简单的实例化启发式方法可以解决它.我也尝试用常量添加一些额外的断言,但它没有帮助.
有没有办法解决这些问题？SMT中量化算法的推理极限是什么？