Branch data Line data Source code
1 : : /************************************************************************************[ParseUtils.h]
2 : : Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
3 : : Copyright (c) 2007-2010, Niklas Sorensson
4 : :
5 : : Permission is hereby granted, free of charge, to any person obtaining a copy of
6 : : this software and associated documentation files (the "Software"), to deal in
7 : : the Software without restriction, including without limitation the rights to
8 : : use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
9 : : the Software, and to permit persons to whom the Software is furnished to do so,
10 : : subject to the following conditions:
11 : :
12 : : The above copyright notice and this permission notice shall be included in all
13 : : copies or substantial portions of the Software.
14 : :
15 : : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16 : : IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
17 : : FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
18 : : COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
19 : : IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
20 : : CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
21 : : **************************************************************************************************/
22 : :
23 : : #ifndef Minisat_ParseUtils_h
24 : : #define Minisat_ParseUtils_h
25 : :
26 : : #include <stdio.h>
27 : : #include <stdlib.h>
28 : :
29 : : // #include <zlib.h>
30 : : #include <unistd.h>
31 : :
32 : : namespace cvc5::internal {
33 : : namespace Minisat {
34 : :
35 : : //-------------------------------------------------------------------------------------------------
36 : : // A simple buffered character stream class:
37 : :
38 : : static const int buffer_size = 1048576;
39 : :
40 : : class StreamBuffer
41 : : {
42 : : int in;
43 : : unsigned char buf[buffer_size];
44 : : int pos;
45 : : int size;
46 : :
47 : : void assureLookahead()
48 : : {
49 : : if (pos >= size)
50 : : {
51 : : pos = 0;
52 : : size = read(in, buf, sizeof(buf));
53 : : }
54 : : }
55 : :
56 : : public:
57 : : explicit StreamBuffer(int i) : in(i), pos(0), size(0) { assureLookahead(); }
58 : :
59 : : int operator*() const { return (pos >= size) ? EOF : buf[pos]; }
60 : : void operator++()
61 : : {
62 : : pos++;
63 : : assureLookahead();
64 : : }
65 : : int position() const { return pos; }
66 : : };
67 : :
68 : : //-------------------------------------------------------------------------------------------------
69 : : // End-of-file detection functions for StreamBuffer and char*:
70 : :
71 : : static inline bool isEof(StreamBuffer& in) { return *in == EOF; }
72 : : static inline bool isEof(const char* in) { return *in == '\0'; }
73 : :
74 : : //-------------------------------------------------------------------------------------------------
75 : : // Generic parse functions parametrized over the input-stream type.
76 : :
77 : : template <class B>
78 : : static void skipWhitespace(B& in)
79 : : {
80 : : while ((*in >= 9 && *in <= 13) || *in == 32) ++in;
81 : : }
82 : :
83 : : template <class B>
84 : : static void skipLine(B& in)
85 : : {
86 : : for (;;)
87 : : {
88 : : if (isEof(in)) return;
89 : : if (*in == '\n')
90 : : {
91 : : ++in;
92 : : return;
93 : : }
94 : : ++in;
95 : : }
96 : : }
97 : :
98 : : template <class B>
99 : : static int parseInt(B& in)
100 : : {
101 : : int val = 0;
102 : : bool neg = false;
103 : : skipWhitespace(in);
104 : : if (*in == '-')
105 : : neg = true, ++in;
106 : : else if (*in == '+')
107 : : ++in;
108 : : if (*in < '0' || *in > '9')
109 : : fprintf(stderr, "PARSE ERROR! Unexpected char: %c\n", *in), exit(3);
110 : : while (*in >= '0' && *in <= '9') val = val * 10 + (*in - '0'), ++in;
111 : : return neg ? -val : val;
112 : : }
113 : :
114 : : // String matching: in case of a match the input iterator will be advanced the
115 : : // corresponding number of characters.
116 : : template <class B>
117 : 0 : static bool match(B& in, const char* str)
118 : : {
119 : : int i;
120 [ - - ]: 0 : for (i = 0; str[i] != '\0'; i++)
121 [ - - ]: 0 : if (in[i] != str[i]) return false;
122 : :
123 : 0 : in += i;
124 : :
125 : 0 : return true;
126 : : }
127 : :
128 : : // String matching: consumes characters eagerly, but does not require random
129 : : // access iterator.
130 : : template <class B>
131 : : static bool eagerMatch(B& in, const char* str)
132 : : {
133 : : for (; *str != '\0'; ++str, ++in)
134 : : if (*str != *in) return false;
135 : : return true;
136 : : }
137 : :
138 : : //=================================================================================================
139 : : } // namespace Minisat
140 : : } // namespace cvc5::internal
141 : :
142 : : #endif
|
