Function flatten_constraint 

fn flatten_constraint<'a, T: Types>(
    constraint: &'a Constraint<T>,
    vars: &mut Vec<(&'a T::Var, &'a Sort<T>)>,
    guards: &mut Vec<&'a Pred<T>>,
    clauses: &mut Vec<HornClause<'a, T>>,
)

Collect all Horn clauses from a constraint tree