Module Elim_ite

module Elim_ite: sig .. end

Eliminate "if/then/else"

Example: if a&b then case else if c&d then case2 else case3 becomes (a&b) => case1; (not (a&b) & c&d) => case2; (not(a&b) & not (c&d)) => case3

type term = Nunchaku_core.FO.T.t

type ty = Nunchaku_core.FO.Ty.t

type problem = (term, ty) Nunchaku_core.FO.Problem.t

val name : string

val transform_term : term -> term

transform a propositional term into a conjunction of condition => term, where each condition is orthogonal to the previous ones

val transform_statement : (term, ty) Nunchaku_core.FO.statement ->
       (term, ty) Nunchaku_core.FO.statement

val transform_problem : problem -> problem

val pipe : print:bool ->
       (problem, problem, 'a, 'a) Nunchaku_core.Transform.t