(declare color type)
(declare A color)
(declare B color)
; formula f is an interpolant for (A,B)
(declare interpolant (! f formula type))
; input formula f is from "c", where c is A|B
(declare color_atom (! c color (! f formula type)))
; simplify interpolant
(program simplify_f ((f formula)) formula
(match f
((and f1 f2)
(let f1' (simplify_f f1)
(match f1'
(true (simplify_f f2))
(false false)
(default
(let f2' (simplify_f f2)
(match f2'
(true f1')
(false false)
(default (and f1' f2'))))))))
((or f1 f2)
(let f1' (simplify_f f1)
(match f1'
(true true)
(false (simplify_f f2))
(default
(let f2' (simplify_f f2)
(match f2'
(true true)
(false f1')
(default (or f1' f2'))))))))
((impl f1 f2)
(let f1' (simplify_f f1)
(match f1'
(true (simplify_f f2))
(false true)
(default
(let f2' (simplify_f f2)
(match f2'
(true true)
(false (match f1'
((not f1'') f1'')
(default (not f1'))))
(default (impl f1' f2'))))))))
((not f1)
(let f1' (simplify_f f1)
(match f1'
((not f1'') f1'')
(default (not f1')))))
(default f)))
(declare simplify_interpolant
(! f formula
(! f' formula
(! i (interpolant f)
(! u (^ (simplify_f f) f')
(interpolant f'))))))