nodes: 0, module; 1, function_definition; 2, function_name:FPS; 3, parameters; 4, block; 5, identifier:name; 6, identifier:sort; 7, default_parameter; 8, expression_statement; 9, expression_statement; 10, return_statement; 11, identifier:explicit_name; 12, None; 13, comment:"""
      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.
      """; 14, assignment; 15, call; 16, identifier:n; 17, call; 18, identifier:FP; 19, argument_list; 20, identifier:_make_name; 21, argument_list; 22, string; 23, tuple; 24, keyword_argument; 25, keyword_argument; 26, keyword_argument; 27, identifier:name; 28, attribute; 29, conditional_expression:False if explicit_name is None else explicit_name; 30, keyword_argument; 31, string_content:FPS; 32, identifier:n; 33, identifier:sort; 34, identifier:variables; 35, set; 36, identifier:symbolic; 37, True; 38, identifier:length; 39, attribute; 40, identifier:sort; 41, identifier:length; 42, False; 43, comparison_operator:explicit_name is None; 44, identifier:explicit_name; 45, identifier:prefix; 46, string; 47, identifier:n; 48, identifier:sort; 49, identifier:length; 50, identifier:explicit_name; 51, None; 52, string_content:FP_
code: def FPS(name, sort, explicit_name=None):
      """
      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.
      """
  
      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)