code: def FPS(name, sort, explicit_name=None):
      
  
      n = _make_name(name, sort.length, False if explicit_name is None else explicit_name, prefix='FP_')
      return FP('FPS', (n, sort), variables={n}, symbolic=True, length=sort.length)
docs: Creates a floating-point symbol.
  
      :param name:            The name of the symbol
      :param sort:            The sort of the floating point
      :param explicit_name:   If False, an identifier is appended to the name to ensure uniqueness.
      :return:                An FP AST.