1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2017 SRI International. 4 * 5 * Yices is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * Yices is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 /* 20 * UTILITIES TO PARSE STRINGS 21 */ 22 23 #ifndef __STRING_UTILS_H 24 #define __STRING_UTILS_H 25 26 #include <stdbool.h> 27 #include <stdint.h> 28 29 30 /* 31 * Binary search in a sorted array of strings. 32 * - a must be sorted in lexicographic order (i.e., 33 * strcmp(a[i], a[i+1]) must be non-negative). 34 * - n = size of the array. n must be > 0 35 * - s = string to search for 36 * 37 * Return the index i such that a[i] = s if s is in the array. 38 * Return -1 otherwise. 39 */ 40 extern int32_t binary_search_string(const char *s, const char * const *a, int32_t n); 41 42 43 /* 44 * Parse s as a keyword: 45 * - a must be an array of strings sorted in lexicographic order 46 * - b must be an array of integer codes of same size as a 47 * - n = size of a and b (n must be positive) 48 * - s = string to search for 49 * If s is equal to a[i] for some i in 0 .. n-1, then 50 * the function returns b[i]. 51 * 52 * Otherwise, return -1. 53 */ 54 extern int32_t parse_as_keyword(const char *s, const char * const *a, const int32_t *b, int32_t n); 55 56 57 /* 58 * Parse s as a boolean: "true" or "TRUE" or "false" or "FALSE" 59 * - store the result in *val 60 * Return code: 61 * - valid_boolean means correct 62 * - invalid_boolean means wrong format 63 */ 64 typedef enum { 65 valid_boolean, 66 invalid_boolean, 67 } boolean_parse_code_t; 68 69 extern boolean_parse_code_t parse_as_boolean(const char *s, bool *val); 70 71 72 /* 73 * Parse s as a decimal number in the format recognized by strtol 74 * <optional_signs><digits> 75 * and store the corresponding number into val 76 * 77 * Return code: 78 * - valid_integer means correct format, no overflow 79 * - integer_overflow means correct format but overflow 80 * - invalid_integer means wrong format 81 */ 82 typedef enum { 83 valid_integer, 84 integer_overflow, 85 invalid_integer, 86 } integer_parse_code_t; 87 88 extern integer_parse_code_t parse_as_integer(const char *s, int32_t *val); 89 90 91 /* 92 * Parse s as an unsigned integer 93 * - decimal, hexa, octal formats are allowed (as supported by strtoul) 94 * 95 * Same return codes as the previous function. 96 */ 97 extern integer_parse_code_t parse_as_uint(const char *s, uint32_t *val); 98 99 100 /* 101 * Parse s as a floating point number in the format recognized by 102 * strtod, and store the corresponding number into val 103 * 104 * Return code: 105 * - valid_double means correct format, no overflow 106 * - double_overflow means correct format but overflow 107 * - invalid_double means wrong format 108 */ 109 typedef enum { 110 valid_double, 111 double_overflow, 112 invalid_double, 113 } double_parse_code_t; 114 115 extern double_parse_code_t parse_as_double(const char *s, double *val); 116 117 118 119 #endif /* __STRING_UTILS_H */ 120