# SMT solving with less-than theory and monotonic functions

I am attempting to solve a less-than theory within an SMT paradigm that involves variables assigned to reals and assumes that all the functions used in the theory are monotonic. The theory's signature has the terms denoted as T and the formulas are denoted as φ. The syntax is given as follows:

$$T = x \mid f(T) \tag{1}$$ $$φ = T < T \mid ¬φ \mid φ ∧ φ \mid φ ∨ φ \tag{2}$$

An example formula in this domain is:

$$(x < y) ∧ (y < z) ∧ ((f(z) < f(y)) ∨ (f(x) < f(z)))$$

How would I begin thinking about how to encode a general formula within the less-than theory as a SAT problem? What is the decision process and encoding algorithm?

1. Directly add $$\forall xy (x < y \Rightarrow f(x) < f(y))$$.