Can iZ3 be used to extract symmetric interpolants

Question

I would like to know how iZ3 can be used to extract symmetric interpolants. Internally iZ3 uses FOCI and FOCI does have symmetric interpolant extraction. FOCI does not accept smt format So i wanted to know if there is any method of extracting symmetric interpolants from iz3 itself

Thanks in advance

Answer 1

You can get symmetric interpolants as a special case of tree interpolants. Here's an example:

(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)))))

Here is z3's output:

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

Have a look at the tutorial at http://rise4fun.com/iZ3/tutorial/guide under "Tree interpolants".