Other mathematical solvers, such as z3 or cplex, are able to solve mathematical models with multiple constraints with the purpose to minimize/maximize an expression, such as:
a+b=10; 2<=b<=6
objective: minimize(a)=> a:=4
However, I can't seem to find any such options in the cvc5 specification. Am I missing something, or does this feature simply not exist?
Currently we're using cplex for such an application, but we're trying to find a solver which isn't as expensive and is deterministic (unlike z3)
To the best of my knowledge CVC5 does not support optimization. For optimizing bit-vectors, you can use the incremental interface by walking down from the most-to-least significant bit. For other theories, you can use quantified formulae. But there is no built-in support for optimization.
Since z3 doesn't seem to work for you, you might want to look at OptiMathSAT, which is purpose built for optimization modulo theories: https://optimathsat.disi.unitn.it
I should note that OptiMathSat (following MathSat) has a rather restrictive license. (Free for research and evaluation purposes only.)