I am trying to use Z3 (SMT solver) to verify and rank a list of solutions. In verification system,I have some constraints and evaluation criteria and based on that I wanted to rank the solution using SMT solver. My question is, can Z3-SMT solver rank the list of solution based on some criteria as in my limited understanding SMT solver are Boolean? I am not only interested in yes/no solution but rank the solution based on solver. Any literature source for this kind of situation can be helpful, as I am from another domain.
Edit: Ranking can be thought as score to different solution. For example, lets assume we have 2 solution and both are feasible but among them I want to select only 1 solution. To do that I am thinking to use Solver to assign some kind of score to solution, so that among multiple feasible solution I can select best solution based on score. Its like ranking of students in classroom.
It's impossible to opine without exactly knowing what this "ranking" precisely involves. Assuming it's some sort of a "cost function" associated with each solution, you can ask an optimizing SMT solver to minimize/maximize that cost function. So, if you can express this "ranking" as a numeric value associated with a solution, you can ask z3 to return a solution that has the maximum (or minimum) such value. Note that z3 can only optimize linear functions; so if your "ranking" involves any sort of non-linearity, it won't work.
For details see: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-optimization
Aside from z3, MathSAT can also do optimization as well, using a different approach: https://optimathsat.disi.unitn.it. Might be worth a try if z3 doesn't perform well.