I want to reason about natural numbers in my constraints.
I know that I can do something like:
x = Int('x') and then add a constraint that x >= 0. But is there a better way of doing this so that I don't have to add an additional constraint every time I declare a variable?
There's no "good" way to model naturals, unfortunately. Your best bet is to add >= 0 constraints as needed. Note that you need to do this after every mathematical operation, especially subtraction.
If machine arithmetic is acceptable (i.e., modulo 2^n for some n; typically n=32 or n=64), then bit-vectors go far. Note that in SMTLib bit-vectors are unsigned, only the operations are. So you can get away without putting extra constraints of the form >= 0 all the time. See Is there an UnsignedIntSort in Z3? for a discussion.