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