标签: cvc4

我在以下看似微不足道的基准测试中尝试了几个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中量化算法的推理极限是什么？

我一直在寻找各种SMT求解器,主要是Z3,CVC4和VeriT.他们都有模糊描述他们用量词解决SMT问题的能力.他们的文档主要是基于示例的(Z3),或由学术论文组成,描述可能或可能不实际实现的可能变更.

我知道有一阶逻辑的可判定片段,例如:

• 有限限定量词
• Monadic一阶逻辑

我想知道的是,哪些(如果有的话)FOL类是保证完整的各种SMT求解器？我怎么知道我正在看的问题是否在他们完成的片段中？

我注意到有一些 SMT2 基准测试，像(_ bv0 32), (_ bv16 32), ... 这样的符号被使用，例如，在：

QF_FP/schanda/spark/zeros_consistent_2.smt2

http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_wp_vdir.rev_xstrcoll_mtime.il.wp.smt2

http://rise4fun.com/Z3/e1s

但是，这不是在理论声明中提及此类符号：

http://smtlib.cs.uiowa.edu/theories.shtml

对此有何评论？它们的含义是什么？

谢谢 ！

我想证明一种简化方法，其中涉及计算以2为底的对数。z3 / cvc4中是否有任何函数可用于计算它？