Formula.cpp

Go to the documentation of this file.
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 <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     /*            0             1             2             3             4             5             6             7             */
00046     /*            XOR           OR            AND           NOT           (             )             i             $             */
00047     /* 0 XOR */ { 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     /* 1 OR  */ { 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     /* 2 AND */ { 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     /* 3 NOT */ { 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     /* 4 (   */ { 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     /* 5 )   */ { 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     /* 6 i   */ { 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     /* 7 $   */ { 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:  /* 0 XOR */ return 0;
00060       case T_OR:   /* 1 OR  */ return 1;
00061       case T_AND:  /* 2 AND */ return 2;
00062       case T_NOT:  /* 3 NOT */ return 3;
00063       case T_LPAR: /* 4 (   */ return 4;
00064       case T_RPAR: /* 5 )   */ return 5;
00065 
00066       case T_VARIABLE:
00067       case T_FALSE:
00068       case T_TRUE:
00069                    /* 6 i   */
00070                                return 6;
00071 
00072       case T_DELIM:
00073       case T_EOF:
00074       case T_STACK_BOTTOM:
00075                    /* 7 $   */
00076                                return 7;
00077 
00078       default:
00079                                // Out of range
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       // Out of range
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     // FIXME: not sure while copy-pasting
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       // TODO: Copy warning from original code
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           // return one before last
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           // Insert '<' after last terminal
00291           stack.insertLt();
00292         case T_PARSER_EQ:
00293           // Insert token to stack
00294           stack.push(token);
00295           break;
00296 
00297         case T_PARSER_GT:
00298           // Reduction
00299 
00300           switch (topTerm.m_token) {
00301             case T_FALSE:
00302             case T_TRUE:
00303             case T_VARIABLE:
00304               {
00305                 // Operand reduction
00306                 Token opToken = stack.pop();
00307                 if (!stack.popAndCompare(T_PARSER_LT)) {
00308                   // Invalid expression
00309                   d->errorDetected = true;
00310                   return T_ERR_EXPR;
00311                 }
00312 
00313                 // Handle operand
00314                 d->cmdList << opToken;
00315                 //std::cerr << "<<< Execute command: " << opToken << std::endl;
00316               }
00317               break;
00318 
00319             case T_RPAR:
00320                 // Parthesis reduction
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                   // Error in parenthesis
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                 // Unary operator NOT
00340                 if (!stack.popAndCompare(T_PARSER_EXPR)) {
00341                   // operand expected
00342                   d->errorDetected = true;
00343                   return T_ERR_EXPR;
00344                 }
00345 
00346                 Token t = stack.pop();
00347                 // Handle token
00348                 d->cmdList << t;
00349                 //std::cerr << "<<< Execute command: " << t << std::endl;
00350 
00351                 if (!stack.popAndCompare(T_PARSER_LT)) {
00352                   // invalid expression
00353                   d->errorDetected = true;
00354                   return T_ERR_EXPR;
00355                 }
00356               }
00357               break;
00358 
00359             default:
00360               {
00361                 // Binary operator
00362                 if (!stack.popAndCompare(T_PARSER_EXPR)) {
00363                   // operand expected
00364                   d->errorDetected = true;
00365                   return T_ERR_EXPR;
00366                 }
00367 
00368                 Token t = stack.pop();
00369                 // Handle token
00370                 d->cmdList << t;
00371                 //std::cerr << "<<< Execute command: " << t << std::endl;
00372 
00373                 if (!stack.popAndCompare(T_PARSER_EXPR)) {
00374                   // operand expected
00375                   d->errorDetected = true;
00376                   return T_ERR_EXPR;
00377                 }
00378 
00379                 if (!stack.popAndCompare(T_PARSER_LT)) {
00380                   // invalid expression
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           // End of expression
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           // Invalid token sequence
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       } // switch
00410     } while (T_PARSER_GT == mode);
00411     // TODO
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     // Check stack size (should be 1)
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 } // namespace FastSatSolver
00457 

Generated on Wed Nov 5 22:30:21 2008 for Fast SAT Solver by  doxygen 1.5.4