code: def satisfiable(self, extra_constraints=(), solver=None, model_callback=None):
          
          return self._satisfiable(extra_constraints=self.convert_list(extra_constraints), solver=solver, model_callback=model_callback)
docs: This function does a constraint check and checks if the solver is in a sat state.
  
          :param solver:              The backend solver object.
          :param extra_constraints:   Extra constraints (as ASTs) to add to s for this solve
          :param model_callback:      a function that will be executed with recovered models (if any)
          :return:                    True if sat, otherwise false