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.