00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include <assert.h>
00021 #include <iostream>
00022 #include <sstream>
00023 #include <vector>
00024 #include <stack>
00025 #include <list>
00026 #include "fssIO.h"
00027 #include "SatSolver.h"
00028 #include "Formula.h"
00029
00030 using std::string;
00031
00032 namespace FastSatSolver {
00033
00034 typedef std::stack<bool> TRuntimeStack;
00035
00039 static const int TABLE_SIZE = 8;
00040
00044 static const EToken table[TABLE_SIZE][TABLE_SIZE] = {
00045
00046
00047 { T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_LT, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
00048 { T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_LT, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
00049 { T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_LT, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
00050 { T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_LT, T_PARSER_LT, T_PARSER_GT, T_PARSER_LT, T_PARSER_GT, },
00051 { T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, T_PARSER_EQ, T_PARSER_LT, T_PARSER_INV, },
00052 { T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_INV, T_PARSER_GT, T_PARSER_INV, T_PARSER_GT, },
00053 { T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_GT, T_PARSER_INV, T_PARSER_GT, T_PARSER_INV, T_PARSER_GT, },
00054 { T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, T_PARSER_LT, T_PARSER_INV, T_PARSER_LT, T_EOF, },
00055 };
00056
00057 inline int tableGetIndex(EToken e) {
00058 switch (e) {
00059 case T_XOR: return 0;
00060 case T_OR: return 1;
00061 case T_AND: return 2;
00062 case T_NOT: return 3;
00063 case T_LPAR: return 4;
00064 case T_RPAR: return 5;
00065
00066 case T_VARIABLE:
00067 case T_FALSE:
00068 case T_TRUE:
00069
00070 return 6;
00071
00072 case T_DELIM:
00073 case T_EOF:
00074 case T_STACK_BOTTOM:
00075
00076 return 7;
00077
00078 default:
00079
00080 return -1;
00081 }
00082 }
00083
00084 inline EToken tableLookup(EToken topTerm, EToken input) {
00085 const int i = tableGetIndex(topTerm);
00086 const int j = tableGetIndex(input);
00087 if (i<0 || j<0)
00088
00089 return T_PARSER_INV;
00090
00091 EToken result = table[i][j];
00092 #if 0//ndef NDEBUG
00093 std::cerr << "tableLookup(" << i << ", " << j << ") = " << result << std::endl;
00094 #endif // NDEBUG
00095 return result;
00096 }
00097
00098 inline bool isTokenTerminal (Token token) {
00099
00100 return (token.m_token < T_PARSER_EXPR);
00101 }
00102
00103 class ParserStack {
00104 public:
00105 void push(Token token) {
00106 container_.push_back(token);
00107 }
00108
00109
00110 void insertLt() {
00111 Token last = container_.back();
00112 if (isTokenTerminal(last))
00113 container_.push_back(T_PARSER_LT);
00114 else {
00115 Token last = container_.back();
00116 container_.pop_back();
00117 container_.push_back(T_PARSER_LT);
00118 container_.push_back(last);
00119 }
00120 }
00121
00122 Token top() {
00123 return container_.back();
00124 }
00125
00126 Token pop() {
00127 Token last = container_.back();
00128 container_.pop_back();
00129 return last;
00130 }
00131
00132 bool popAndCompare(EToken e) {
00133 Token t = this->pop();
00134 return t.m_token == e;
00135 }
00136
00137 Token topTerm() {
00138 size_t size = container_.size();
00139 Token last = container_.back();
00140 if (isTokenTerminal(last))
00141 return last;
00142 else
00143
00144 return container_[size-2];
00145 }
00146
00147 private:
00148 typedef std::vector<Token> TContainer;
00149 TContainer container_;
00150 };
00151
00152 class Cmd {
00153 public:
00154 static Cmd* fromToken(Token token);
00155 virtual ~Cmd() { }
00156 virtual void execute(TRuntimeStack *, ISatItem *) = 0;
00157 protected:
00158 Cmd() { }
00159 };
00160 class CmdConstant: public Cmd {
00161 public:
00162 CmdConstant(bool value): b(value) { }
00163 virtual void execute(TRuntimeStack *stack, ISatItem *) {
00164 stack->push(b);
00165 }
00166 private:
00167 bool b;
00168 };
00169 class CmdVariable: public Cmd {
00170 public:
00171 CmdVariable(int varId): id(varId) { }
00172 virtual void execute(TRuntimeStack *stack, ISatItem *data) {
00173 assert(id >= 0);
00174 assert(id < data->getLength());
00175 bool b = data->getBit(id);
00176 stack->push(b);
00177 }
00178 private:
00179 int id;
00180 };
00181 class CmdUnaryNot: public Cmd {
00182 public:
00183 virtual void execute(TRuntimeStack *stack, ISatItem *) {
00184 assert(!stack->empty());
00185 bool b = stack->top();
00186 stack->pop();
00187 stack->push(!b);
00188 }
00189 };
00190 class CmdBinary: public Cmd {
00191 public:
00192 CmdBinary(EToken e): et(e) { }
00193 virtual void execute(TRuntimeStack *stack, ISatItem *) {
00194 assert(!stack->empty());
00195 bool a = stack->top();
00196 stack->pop();
00197
00198 assert(!stack->empty());
00199 bool b = stack->top();
00200 stack->pop();
00201
00202 bool c;
00203 switch (et) {
00204 case T_AND: c = a & b; break;
00205 case T_OR: c = a | b; break;
00206 case T_XOR: c = a ^ b; break;
00207 default:
00208 {
00209 std::ostringstream stream;
00210 stream << "CmdBinary::execute(): unknown token: " << et;
00211 throw GenericException(stream.str());
00212 }
00213 }
00214 stack->push(c);
00215 }
00216 private:
00217 EToken et;
00218 };
00219 Cmd* Cmd::fromToken(Token token) {
00220 switch (token.m_token) {
00221 case T_FALSE: return new CmdConstant(false);
00222 case T_TRUE: return new CmdConstant(true);
00223 case T_VARIABLE: return new CmdVariable(token.m_ext_number);
00224 case T_NOT: return new CmdUnaryNot;
00225 case T_AND:
00226 case T_OR:
00227 case T_XOR:
00228 return new CmdBinary(token.m_token);
00229 default:
00230 {
00231 std::ostringstream stream;
00232 stream << "Cmd::fromToken(): unknown token: " << token;
00233 throw GenericException(stream.str());
00234 }
00235 }
00236 }
00237 class CmdList: public Cmd {
00238 public:
00239 virtual ~CmdList() {
00240 TContainer::iterator iter;
00241 for(iter=container_.begin(); iter!=container_.end(); iter++)
00242 delete *iter;
00243 }
00244 virtual void execute(TRuntimeStack *stack, ISatItem *data) {
00245 TContainer::iterator iter;
00246 for(iter=container_.begin(); iter!=container_.end(); iter++) {
00247 Cmd *cmd = *iter;
00248 cmd->execute(stack, data);
00249 }
00250 }
00251 void operator<< (Cmd *cmd) {
00252 container_.push_back(cmd);
00253 }
00254 void operator<< (const Token &token) {
00255 operator<< (Cmd::fromToken(token));
00256 }
00257 private:
00258 typedef std::list<Cmd *> TContainer;
00259 TContainer container_;
00260 };
00261
00262 struct InterpretedFormula::Private {
00263 ParserStack parserStack;
00264 bool errorDetected;
00265 CmdList cmdList;
00266 };
00267
00268 InterpretedFormula::InterpretedFormula():
00269 d(new Private)
00270 {
00271 d->parserStack.push(T_STACK_BOTTOM);
00272 d->errorDetected = false;
00273 }
00274
00275 InterpretedFormula::~InterpretedFormula() {
00276 delete d;
00277 }
00278
00282 int InterpretedFormula::parse (Token token ) {
00283 ParserStack &stack = d->parserStack;
00284 EToken mode;
00285 do {
00286 Token topTerm = stack.topTerm();
00287 mode = tableLookup(topTerm.m_token, token.m_token);
00288 switch (mode) {
00289 case T_PARSER_LT:
00290
00291 stack.insertLt();
00292 case T_PARSER_EQ:
00293
00294 stack.push(token);
00295 break;
00296
00297 case T_PARSER_GT:
00298
00299
00300 switch (topTerm.m_token) {
00301 case T_FALSE:
00302 case T_TRUE:
00303 case T_VARIABLE:
00304 {
00305
00306 Token opToken = stack.pop();
00307 if (!stack.popAndCompare(T_PARSER_LT)) {
00308
00309 d->errorDetected = true;
00310 return T_ERR_EXPR;
00311 }
00312
00313
00314 d->cmdList << opToken;
00315
00316 }
00317 break;
00318
00319 case T_RPAR:
00320
00321 stack.pop();
00322 if (
00323 !stack.popAndCompare(T_PARSER_EXPR) ||
00324 !stack.popAndCompare(T_LPAR) ||
00325 !stack.popAndCompare(T_PARSER_LT)
00326 )
00327 {
00328
00329 d->errorDetected = true;
00330 return T_ERR_EXPR;
00331 }
00332 #if 0//ndef NDEBUG
00333 std::cerr << "Droping brackets..." << std::endl;
00334 #endif // NDEBUG
00335 break;
00336
00337 case T_NOT:
00338 {
00339
00340 if (!stack.popAndCompare(T_PARSER_EXPR)) {
00341
00342 d->errorDetected = true;
00343 return T_ERR_EXPR;
00344 }
00345
00346 Token t = stack.pop();
00347
00348 d->cmdList << t;
00349
00350
00351 if (!stack.popAndCompare(T_PARSER_LT)) {
00352
00353 d->errorDetected = true;
00354 return T_ERR_EXPR;
00355 }
00356 }
00357 break;
00358
00359 default:
00360 {
00361
00362 if (!stack.popAndCompare(T_PARSER_EXPR)) {
00363
00364 d->errorDetected = true;
00365 return T_ERR_EXPR;
00366 }
00367
00368 Token t = stack.pop();
00369
00370 d->cmdList << t;
00371
00372
00373 if (!stack.popAndCompare(T_PARSER_EXPR)) {
00374
00375 d->errorDetected = true;
00376 return T_ERR_EXPR;
00377 }
00378
00379 if (!stack.popAndCompare(T_PARSER_LT)) {
00380
00381 d->errorDetected = true;
00382 return T_ERR_EXPR;
00383 }
00384 }
00385 }
00386 stack.push(T_PARSER_EXPR);
00387 break;
00388
00389 case T_EOF:
00390
00391 d->errorDetected = !(this->isValid());
00392 if (d->errorDetected)
00393 return T_ERR_EXPR;
00394 else
00395 return 0;
00396
00397 case T_PARSER_INV:
00398
00399 d->errorDetected = true;
00400 return T_ERR_EXPR;
00401
00402 default:
00403 {
00404 d->errorDetected = true;
00405 std::ostringstream stream;
00406 stream << "Unexpected symbol in precedence table: " << mode;
00407 throw GenericException(stream.str());
00408 }
00409 }
00410 } while (T_PARSER_GT == mode);
00411
00412 return 0;
00413 }
00414
00418 bool InterpretedFormula::isValid ( ) {
00419 ParserStack &stack = d->parserStack;
00420 Token topTerm = stack.topTerm();
00421 Token top = stack.top();
00422 #if 0//ndef NDEBUG
00423 std::cerr << "InterpretedFormula::isValid(): topTerm = " << topTerm;
00424 std::cerr << "InterpretedFormula::isValid(): top = " << top;
00425 std::cerr << "InterpretedFormula::isValid(): errorDetected = " << d->errorDetected << std::endl;
00426 std::cerr << std::endl;
00427 #endif // NDEBUG
00428 return
00429 topTerm.m_token == T_STACK_BOTTOM &&
00430 top.m_token == T_PARSER_EXPR &&
00431 !(d->errorDetected);
00432 }
00433
00437 bool InterpretedFormula::eval (ISatItem *data) {
00438 if (!this->isValid())
00439 throw GenericException("InterpretedFormula::eval(): called for invalid formula");
00440
00441 TRuntimeStack stack;
00442 d->cmdList.execute(&stack, data);
00443
00444
00445 const int stackSize = stack.size();
00446 if (1!=stackSize) {
00447 std::ostringstream stream;
00448 stream << "InterpretedFormula::eval(): incorrect stack size after cmdList.execute(): " << stackSize;
00449 throw GenericException(stream.str());
00450 }
00451
00452 return stack.top();
00453 }
00454
00455
00456 }
00457