Можно ли использовать iZ3 для извлечения симметричных интерполантов

Question

Можно ли использовать iZ3 для извлечения симметричных интерполантов

Я хотел бы знать, как iZ3 может использоваться для извлечения симметричных интерполантов. Внутренне iZ3 использует FOCI, а FOCI имеет симметричное интерполяционное извлечение. FOCI не принимает формат smt. Поэтому я хотел бы знать, есть ли какой-либо метод извлечения симметричных интерполантов из самого iz3

заранее спасибо

0

z3 smt

Источник

user2955638 22 янв '14 в 02:22

1 ответ

Решение

Другие вопросы по тегам z3 smt

user1214978 23 янв '14 в 19:31 2014-01-23 19:31 · Accepted Answer · 2014-01-23 19:31

Вы можете получить симметричные интерполанты в качестве частного случая интерполяции дерева. Вот пример:

(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 разделе "Дерево интерполяторов".