Quantifier-free encoding of invariants for hybrid systems