Module Model_clean

module Model_clean: sig .. end

Cleanup models

rename values to something more "canonical"
eliminate recursive definitions in decision trees

type term = Nunchaku_core.TermInner.Default.t

type model = (term, term) Nunchaku_core.Model.t

val name : string

val rename : model -> model

rename m performs a renaming of domain constants and bound variables that should be regular and readable. Assumes the types that have finite domains are ground types.
Raises Invalid_argument if some assumption is invalidated

val remove_recursion : model -> model

remove_recursion m transforms definitions such as f x = if x=0 then 0 else if x=1 then f 0 else ... into f x = if x=0 then 0 else if x=1 then 0 else ...

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