00001 /* 00002 * Copyright (C) 2008 Kamil Dudka <xdudka00@stud.fit.vutbr.cz> 00003 * 00004 * This file is part of fss (Fast SAT Solver). 00005 * 00006 * fss is free software: you can redistribute it and/or modify 00007 * it under the terms of the GNU General Public License as published by 00008 * the Free Software Foundation, either version 3 of the License, or 00009 * any later version. 00010 * 00011 * fss is distributed in the hope that it will be useful, 00012 * but WITHOUT ANY WARRANTY; without even the implied warranty of 00013 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 00014 * GNU General Public License for more details. 00015 * 00016 * You should have received a copy of the GNU General Public License 00017 * along with fss. If not, see <http://www.gnu.org/licenses/>. 00018 */ 00019 00020 #include <iostream> 00021 #include <string> 00022 #include <map> 00023 #include "SatProblem.h" 00024 #include "Scanner.h" 00025 #include "Formula.h" 00026 00027 using std::string; 00028 00029 namespace FastSatSolver { 00030 00031 // //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// 00032 // RawScanner implementation 00033 struct RawScanner::Private { 00034 enum EState { 00035 STATE_INIT, 00036 STATE_BUILDING_STRING 00037 }; 00038 FILE *fd; 00039 EState state; 00040 int line; 00041 }; 00042 RawScanner::RawScanner (FILE* fd ): 00043 d(new Private) 00044 { 00045 d->fd = fd; 00046 d->state = Private::STATE_INIT; 00047 d->line = 1; 00048 } 00049 RawScanner::~RawScanner() { 00050 delete d; 00051 } 00052 int RawScanner::readNext (Token *token) { 00053 while (1) { 00054 token->m_line = d->line; 00055 int c = fgetc(d->fd); 00056 switch(d->state) { 00057 case Private::STATE_INIT: 00058 token->m_ext_text.clear(); 00059 switch (c) { 00060 case '0': token->m_token = T_FALSE; return 0; 00061 case '1': token->m_token = T_TRUE; return 0; 00062 case '~': token->m_token = T_NOT; return 0; 00063 case '&': token->m_token = T_AND; return 0; 00064 case '|': token->m_token = T_OR; return 0; 00065 case '^': token->m_token = T_XOR; return 0; 00066 case '(': token->m_token = T_LPAR; return 0; 00067 case ')': token->m_token = T_RPAR; return 0; 00068 case ';': token->m_token = T_DELIM; return 0; 00069 case EOF: token->m_token = T_EOF; return 0; 00070 case '\n': 00071 d->line ++; 00072 default: 00073 if (isspace(c)) 00074 // Ignore white characters 00075 break; 00076 00077 if (isalpha(c) || '_'==c) { 00078 // Initiate string building 00079 token->m_ext_text = c; 00080 d->state = Private::STATE_BUILDING_STRING; 00081 break; 00082 } 00083 // Lexical error 00084 token->m_token = T_ERR_LEX; 00085 return 0; 00086 } 00087 break; 00088 00089 case Private::STATE_BUILDING_STRING: 00090 if (isalpha(c) || isdigit(c) || '_'==c) { 00091 // Building string 00092 token->m_ext_text += c; 00093 break; 00094 } 00095 // End of string 00096 ungetc(c, d->fd); 00097 d->state = Private::STATE_INIT; 00098 token->m_token = T_STRING; 00099 return 0; 00100 00101 default: 00102 // Unknown state 00103 return 1; 00104 } 00105 } 00106 } 00107 00108 00109 // //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// 00110 // ScannerStringHandler implementation 00111 struct ScannerStringHandler::Private { 00112 typedef std::map<std::string,EToken> TKeyWordMap; 00113 IScanner *scanner; 00114 VariableContainer *vc; 00115 TKeyWordMap keyWordMap; 00116 }; 00117 ScannerStringHandler::ScannerStringHandler (IScanner *scanner, VariableContainer *vc ): 00118 d(new Private) 00119 { 00120 d->scanner = scanner; 00121 d->vc = vc; 00122 00123 // Keywords definition 00124 d->keyWordMap["NOT"] = T_NOT; 00125 d->keyWordMap["AND"] = T_AND; 00126 d->keyWordMap["OR"] = T_OR; 00127 d->keyWordMap["XOR"] = T_XOR; 00128 d->keyWordMap["FALSE"] = T_FALSE; 00129 d->keyWordMap["TRUE"] = T_TRUE; 00130 } 00131 ScannerStringHandler::~ScannerStringHandler() { 00132 delete d; 00133 } 00134 int ScannerStringHandler::readNext (Token* token ) { 00135 // Use RawScanner to read token 00136 d->scanner->readNext(token); 00137 00138 // Transformations 00139 switch (token->m_token) { 00140 case T_STRING: 00141 // Handle only T_STRING 00142 { 00143 string &text = token->m_ext_text; 00144 if (d->keyWordMap.end() != d->keyWordMap.find(text)) { 00145 // Map T_STRING to keywords 00146 token->m_token = d->keyWordMap[text]; 00147 return 0; 00148 } 00149 00150 // Use string as variable name 00151 token->m_token = T_VARIABLE; 00152 token->m_ext_number = d->vc->addVariable(text); 00153 } 00154 default: 00155 // Default behavior 00156 return 0; 00157 } 00158 } 00159 00160 00161 // //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// 00162 // ScannerFormulaHandler implementation 00163 struct ScannerFormulaHandler::Private { 00164 IScanner *scanner; 00165 FormulaContainer *fc; 00166 InterpretedFormula *current; 00167 bool ignoreToDelim; 00168 }; 00169 ScannerFormulaHandler::ScannerFormulaHandler (IScanner *scanner, FormulaContainer *fc ): 00170 d(new Private) 00171 { 00172 d->scanner = scanner; 00173 d->fc = fc; 00174 d->ignoreToDelim = false; 00175 d->current = new InterpretedFormula; 00176 } 00177 ScannerFormulaHandler::~ScannerFormulaHandler() { 00178 delete d->current; 00179 delete d; 00180 } 00181 int ScannerFormulaHandler::readNext (Token* token ) { 00182 // Use ScannerStringHandler to read token 00183 while (0== d->scanner->readNext(token)) { 00184 switch (token->m_token) { 00185 case T_FALSE: 00186 case T_TRUE: 00187 case T_NOT: 00188 case T_AND: 00189 case T_OR: 00190 case T_XOR: 00191 case T_LPAR: 00192 case T_RPAR: 00193 case T_VARIABLE: 00194 if (d->ignoreToDelim) 00195 // Ignore token 00196 break; 00197 00198 // Parse token by IFormulaBuilder 00199 if (0!= d->current->parse(*token)) { 00200 // Expression error 00201 d->ignoreToDelim = true; 00202 token->m_token = T_ERR_EXPR; 00203 return 0; 00204 } 00205 break; 00206 00207 case T_ERR_LEX: 00208 // Lexical error 00209 if (d->ignoreToDelim) 00210 // Ignore error 00211 break; 00212 d->ignoreToDelim = true; 00213 return 0; 00214 00215 case T_EOF: 00216 case T_DELIM: 00217 d->current -> parse(T_EOF); 00218 if (!d->ignoreToDelim && d->current->isValid()) { 00219 // Formula successfully readed 00220 d->fc->addFormula(d->current); 00221 d->current = new InterpretedFormula; 00222 #if 0//ndef NDEBUG 00223 std::cerr << ">>> Formula red successfully" << std::endl; 00224 #endif // NDEBUG 00225 if (T_DELIM==token->m_token) 00226 break; 00227 else 00228 return 0; 00229 } 00230 if (T_EOF==token->m_token) 00231 return 0; 00232 00233 // Error recover 00234 #ifndef NDEBUG 00235 std::cerr << "--- Error recover" << std::endl; 00236 #endif // NDEBUG 00237 delete d->current; 00238 d->current = new InterpretedFormula; 00239 if (!d->ignoreToDelim) { 00240 // Parse error 00241 token->m_token = T_ERR_PARSE; 00242 return 0; 00243 } 00244 d->ignoreToDelim = false; 00245 break; 00246 00247 default: 00248 return 0; 00249 } 00250 } 00251 // This sohould never happen 00252 return -1; 00253 } 00254 00255 } // namespace FastSatSolver
1.5.4