Are there any solvers that can handle non-linearity?

I need a way to solve linear and non-linear inequalities over the natural numbers. So equations like this should be solveable:

$$\forall n, p, q \in \mathbb{N}. q \cdot (1 + n^p) \leq q$$

From what I gather SMT solver should are a good choice for this. I'm not an expert on the area of SMT solvers so I would like guidance on what solver would be best suited for this task. Wikipedia lists many but it's not clear to me which one I should pick.

Any pointers are appreciated! This will be part of a larger program so I can't use online services.

• wolframalpha.com is a great site that can solve many equations, and do many other things. I dunno if it can do what you specifically want to do with it, but i think its worth taking a look at it Commented Jun 22, 2021 at 11:49
• @nirshahar this will be part of a program. I can't rely on online services. Commented Jun 22, 2021 at 12:11
• z3 is a well known SMT solver and supports non-linear arithmetic, but note that non-linear arithmetic are in general undecidable. Commented Jun 22, 2021 at 14:22
• Please don't delete and re-post closed questions; instead, edit them and then vote to re-open. My comment from before remains valid: Your question is too broad as it doesn't narrow down the set of constraints you want to deal with. "Linear and nonlinear constraints" includes all possible constraints. We can't guide you on picking a solver without more specific information about your requirements.
– D.W.
Commented Jun 22, 2021 at 17:19
• @D.W. It does include all possible constraints over the naturals. Why is that question invalid? I did edit my question. However the question remained closed with the request of either editing my question or reposting a new version. Commented Jun 22, 2021 at 17:40