Yes, Z3 has a solver based on the Simplex method. It is implemented in the files src\smt\theory_arith*
. The main files are src\smt\theory_arith.h
and src\smt\theory_arith_core.h
.
This solver has very basic support for optimization in the file src\smt\theory_arith_aux.h
. This functionality is not "exposed" by the solver. It is used internally in the extensions/heuristics for integer and nonlinear arithmetic.
BTW, recall that Z3 solver is based on rational (precise) arithmetic. So, it is much slower than solvers based on floating point arithmetic. Moreover, this solver does not use the revised simplex method.