Simplex solver in Z3

Question

I'm aware that there is a simplex solver implemented in z3. Is it possible to use the solver for linear optimization? Where is the interface for the solver located in the z3 source code?

Answer 1

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.