I would add an SMT solver like Z3. It can solve problems when they are translated into first order logic.