code: def batch_eval(self, exprs, n, extra_constraints=(), solver=None, model_callback=None):
          
          if self._solver_required and solver is None:
              raise BackendError("%s requires a solver for batch evaluation" % self.__class__.__name__)
  
          converted_exprs = [ self.convert(ex) for ex in exprs ]
  
          return self._batch_eval(
              converted_exprs, n, extra_constraints=self.convert_list(extra_constraints),
              solver=solver, model_callback=model_callback
          )
docs: Evaluate one or multiple expressions.
  
          :param exprs:               A list of expressions to evaluate.
          :param n:                   Number of different solutions to return.
          :param extra_constraints:   Extra constraints (as ASTs) to add to the solver for this solve.
          :param solver:              A solver object, native to the backend, to assist in the evaluation.
          :param model_callback:      a function that will be executed with recovered models (if any)
          :return:                    A list of up to n tuples, where each tuple is a solution for all expressions.