iZ3可以用来提取对称插值吗

【问题标题】：Can iZ3 be used to extract symmetric interpolantsiZ3可以用来提取对称插值吗
【发布时间】：2014-01-22 02:22:31
【问题描述】：

我想知道如何使用 iZ3 来提取对称插值。 iZ3 在内部使用 FOCI，而 FOCI 确实具有对称插值提取。 FOCI 不接受 smt 格式所以我想知道是否有任何方法可以从 iz3 本身中提取对称插值

提前致谢

【问题讨论】：

标签： z3 smt

【解决方案1】：

您可以获得对称插值作为树插值的特例。这是一个例子：

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(compute-interpolant
  (and
    (interp (<= 0 a))
    (interp (and (= a b) (= b c)))
    (interp (and (= c d) (<= d -1)))))

这是 z3 的输出：

unsat
(>= a 0)
(= a c)
(<= c (- 1))

在“树插值”下查看http://rise4fun.com/iZ3/tutorial/guide 的教程。

【讨论】：