- Main Page
- Namespaces
- Classes
- Files
- Related Pages

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/ISAT/ISAT_test.cpp

    00001 //========================================================================================
    00002 //
    00003 // Copyright (c) 2001           Model-based Embedded and Robotic Systems Group
    00004 // All Rights Reserved          Massachusetts Institute of Technology
    00005 //
    00006 // This software is provided as is. Model-based Embedded and Robotic Systems (MERS) group
    00007 // does not assume any responsibility.
    00008 //
    00009 // AUTHOR:                      Seung H. Chung
    00010 //
    00011 // ORGANIZATION:        Model-based Embedded and Robotic Systems Group
    00012 //                                      Massachusetts Institute of Technology
    00013 //
    00014 // FILE:                        ISAT_test.cpp
    00015 //
    00016 // DESCRIPTION:
    00017 //
    00018 //
    00019 //
    00020 //========================================================================================
    00021
    00022 #if defined _MSC_VER
    00023 #pragma warning(disable:4786)
    00024 #endif // #if defined _MSC_VER
    00025
    00026 #include <cassert>
    00027 #include <iostream>
    00028 #include <fstream>
    00029 #include <string>
    00030 #include <vector>
    00031 #include <Mers/Models/CCA/CCAModel.h>
    00032 #include <Mers/Models/CCA/Io/Mof/MOFReader.h>
    00033 #include "ISATStringDescription.h"
    00034 #include "ISATProposition.h"
    00035 #include "ISATLiteral.h"
    00036 #include "ISATClause.h"
    00037 #include "ISATInconsistentClauses.h"
    00038 #include "ISATClauses.h"
    00039 #include "ISATClausesSet.h"
    00040 #include "ISAT.h"
    00041
    00042 using namespace std;
    00043 using namespace Mers::Solvers::SAT::ISAT;
    00044 using Mers::Models::CCA::CCAModel;
    00045 using Mers::Models::CCA::CCAAssignment;
    00046 using Mers::Models::CCA::CCAClause;
    00047 using Mers::Models::CCA::CCASentence;
    00048 using Mers::Models::CCA::Io::Mof::MOFReader;
    00049
    00050 void run_ISAT_shell();
    00051 void run_command(istream &stream);
    00052 void run_parenthesis_command(istream &stream);
    00053 void run_pound_command(istream &stream);
    00054 void run_b_command(istream &stream);
    00055 void run_c_command(istream &stream);
    00056 void run_d_command(istream &stream);
    00057 void run_f_command(istream &stream);
    00058 void run_h_command(istream &stream);
    00059 void run_i_command(istream &stream);
    00060 void run_l_command(istream &stream);
    00061 void run_n_command(istream &stream);
    00062 void run_p_command(istream &stream);
    00063 void run_q_command(istream &stream);
    00064 void run_t_command(istream &stream);
    00065
    00066 void print_ISAT_shell_help(char ch);
    00067 void print_theory_info(char ch);
    00068 void print_clause_index();
    00069 void print_clause(unsigned int i);
    00070 void print_facts();
    00071 void print_counters();
    00072 void print_time();
    00073 void reset_time_and_counters();
    00074
    00075 void activate_clause(unsigned int i);
    00076 void deactivate_clause(unsigned int i);
    00077 void remove_clause(unsigned int i);
    00078 void set_fact(unsigned int i, bool isFact);
    00079
    00080 void eat_space_or_tab(istream &stream);
    00081 void clear_stream(istream &stream);
    00082 //ISATLiteral *read_literal(istream &stream);
    00083
    00084 void load_DIMACS_file(string const *file_name_p);
    00085 void load_DIMACS_CNF_format(ifstream &DIMACS_stream);
    00086 void load_DIMACS_SAT_format(ifstream &DIMACS_stream) {};
    00087 void load_MOF_file(string const *file_name_p);
    00088
    00089 void load_script_file(string const *file_name_p);
    00090
    00091 ISAT                                    SAT_engine;
    00092 vector<ISATClause *>    clauses;
    00093 vector<bool>                    isFactClause;
    00094 ISATClauses                             facts;
    00095 bool                                    use_DPLL;
    00096 bool                                    quit_shell = false;
    00097
    00098 int
    00099 main(int argc, char** argv)
    00100 {
    00101         argc--;
    00102         argv++;
    00103
    00104         run_ISAT_shell();
    00105
    00106         return 0;
    00107 }
    00108
    00109 void
    00110 run_ISAT_shell()
    00111 {
    00112         string  temp_string;
    00113
    00114         cout << endl << "ISAT Shell: Enter 'h' for help.";
    00115         cout << endl << endl;
    00116
    00117         while (!quit_shell)
    00118         {
    00119
    00120                 cout << "> " << flush;
    00121                 run_command(cin);
    00122         }
    00123 }
    00124
    00125 void
    00126 run_command(istream &stream)
    00127 {
    00128         eat_space_or_tab(stream);
    00129         switch (stream.peek())
    00130         {
    00131         case '\n':
    00132                 break;
    00133         case '#':
    00134                 stream.ignore(1);
    00135                 run_pound_command(stream);
    00136                 break;
    00137         case '(':
    00138                 stream.ignore(1);
    00139                 run_parenthesis_command(stream);
    00140                 break;
    00141 #if defined(_DEBUG)
    00142         case 'b':
    00143         case 'B':
    00144                 stream.ignore(1);
    00145                 run_b_command(stream);
    00146                 break;
    00147 #endif // #if defined(_DEBUG)
    00148         case 'c':
    00149         case 'C':
    00150                 stream.ignore(1);
    00151                 run_c_command(stream);
    00152                 break;
    00153                 // 'd' or 'D' corresponds to toggle DPLL on or off.
    00154         case 'd':
    00155         case 'D':
    00156                 stream.ignore(1);
    00157                 run_d_command(stream);
    00158                 break;
    00159                 // 'f' or 'F' adds or deletes facts.
    00160         case 'f':
    00161         case 'F':
    00162                 stream.ignore(1);
    00163                 run_f_command(stream);
    00164                 break;
    00165                 // 'h', 'H', or '?' corresponds to display help menu.
    00166         case 'h':
    00167         case 'H':
    00168         case '?':
    00169                 stream.ignore(1);
    00170                 run_h_command(stream);
    00171                 break;
    00172                 // 'i' or 'I' corresponds to display clause index.
    00173         case 'i':
    00174         case 'I':
    00175                 stream.ignore(1);
    00176                 run_i_command(stream);
    00177                 break;
    00178                 // 'l' or 'L' corresponds to load file.
    00179         case 'l':
    00180         case 'L':
    00181                 stream.ignore(1);
    00182                 run_l_command(stream);
    00183                 break;
    00184                 // 'n' or 'N' corresponds number of times
    00185                 // this command displays timing information
    00186         case 'n':
    00187         case 'N':
    00188                 stream.ignore(1);
    00189                 run_n_command(stream);
    00190                 break;
    00191                 // 'p' or 'P' corresponds to propagate
    00192         case 'p':
    00193         case 'P':
    00194                 stream.ignore(1);
    00195                 run_p_command(stream);
    00196                 break;
    00197                 // 'q' or 'Q' corresponds to quit.
    00198         case 'q':
    00199         case 'Q':
    00200                 stream.ignore(1);
    00201                 run_q_command(stream);
    00202                 break;
    00203         case 't':
    00204         case 'T':
    00205                 stream.ignore(1);
    00206                 run_t_command(stream);
    00207                 break;
    00208         default:
    00209                 if (!stream.eof())
    00210                 {
    00211                         cout << "Invalid command." << endl;
    00212                 }
    00213                 break;
    00214         }
    00215
    00216         clear_stream(stream);
    00217 }
    00218
    00219 void
    00220 run_parenthesis_command(istream & stream)
    00221 {
    00222         ISATStringDescription *prop_desc_p;
    00223         ISATClause *clause_p;
    00224         string  temp_string;
    00225
    00226         clause_p = SAT_engine.insert_new_empty_clause();
    00227         while(stream.peek() != ')')
    00228         {
    00229                 // Read in a literal
    00230                 stream >> temp_string;
    00231                 if (temp_string.rfind(')') == temp_string.size() - 1)
    00232                 {
    00233                         temp_string.erase(temp_string.size() - 1);
    00234                         stream.putback(')');
    00235                 }
    00236
    00237                 if (temp_string != "")
    00238                 {
    00239                         if (*temp_string.begin() == '-')
    00240                         {
    00241                                 temp_string.erase(0,1);
    00242                                 assert(temp_string != "");
    00243                                 prop_desc_p = new ISATStringDescription(&temp_string);
    00244                                 SAT_engine.add_literal_to_new_clause(prop_desc_p, ISATLiteral::NEGATIVE);
    00245                         }
    00246                         else
    00247                         {
    00248                                 assert(temp_string != "");
    00249                                 prop_desc_p = new ISATStringDescription(&temp_string);
    00250                                 SAT_engine.add_literal_to_new_clause(prop_desc_p, ISATLiteral::POSITIVE);
    00251                         }
    00252                 }
    00253                 // Check if Literal signals end of the clause
    00254                 if (stream.peek() == ')' && clause_p->get_numb_of_literals() > 0)
    00255                 {
    00256                         SAT_engine.activate_clause(clause_p);
    00257                         clauses.push_back(clause_p);
    00258                         isFactClause.push_back(false);
    00259                 }
    00260         }
    00261 }
    00262
    00263 void
    00264 run_pound_command(istream & stream)
    00265 {
    00266         return;
    00267 }
    00268
    00269 void
    00270 run_b_command(istream & stream)
    00271 {
    00272         int             i;
    00273         eat_space_or_tab(stream);
    00274         if (stream.peek() == '\n')
    00275         {
    00276                 cout << "Invalid command." << endl;
    00277                 cout << "\tb [NUMBER]" << endl;
    00278         }
    00279         else if (stream.peek() >= '0' && stream.peek() <= '9')
    00280         {
    00281                 stream >> i;
    00282 #ifdef _DEBUG
    00283                 SAT_engine.set_debug_level(i);
    00284 #endif
    00285                 cout << "Debug Level = " << i << endl;
    00286         }
    00287         else if (stream.peek() == '-')
    00288         {
    00289                 stream.ignore();
    00290                 if (stream.peek() != 'h')
    00291                 {
    00292                         print_ISAT_shell_help('b');
    00293                 }
    00294                 else
    00295                 {
    00296                         cout << "Invalid command." << endl;
    00297                         cout << "\tb [NUMBER]" << endl;
    00298                 }
    00299         }
    00300         else
    00301         {
    00302                 cout << "Invalid command." << endl;
    00303                 cout << "\tb [NUMBER]" << endl;
    00304         }
    00305 }
    00306
    00307 void
    00308 run_c_command(istream & stream)
    00309 {
    00310         int             i;
    00311         char    char_array[300];
    00312         string  temp_string;
    00313         eat_space_or_tab(stream);
    00314         if (stream.peek() == '\n')
    00315         {
    00316                 cout << "Invalid command." << endl;
    00317                 cout << "\tc [OPTION] [NUMBER]" << endl;
    00318         }
    00319         else if (stream.peek() >= '0' && stream.peek() <= '9')
    00320         {
    00321                 stream >> i;
    00322                 print_clause(i);
    00323         }
    00324         else if (stream.peek() == '-')
    00325         {
    00326                 stream.ignore(1);
    00327                 stream.get(char_array, 2);
    00328                 eat_space_or_tab(stream);
    00329                 if (stream.peek() >= '0' && stream.peek() <= '9')
    00330                 {
    00331                         stream >> i;
    00332                         switch (char_array[0])
    00333                         {
    00334                         case 'a':
    00335                         case 'A':
    00336                                 activate_clause(i);
    00337                                 break;
    00338                         case 'd':
    00339                         case 'D':
    00340                                 deactivate_clause(i);
    00341                                 break;
    00342                         case 'r':
    00343                         case 'R':
    00344                                 remove_clause(i);
    00345                                 break;
    00346                         default:
    00347                                 cout << "Invalid command." << endl;
    00348                                 cout << "\tc [OPTION] [NUMBER]" << endl;
    00349                                 break;
    00350                         }
    00351                 }
    00352                 else if (char_array[0] == 'r' || char_array[0] == 'R')
    00353                 {
    00354                         temp_string = "";
    00355                         while (temp_string != "yes" && temp_string != "no")
    00356                         {
    00357                                 cout << "Would you like to remove all clauses? [yes/no] ";
    00358                                 stream >> temp_string;
    00359                         }
    00360                         if (temp_string == "yes")
    00361                         {
    00362                                 while (!clauses.empty())
    00363                                 {
    00364                                         remove_clause(0);
    00365                                 }
    00366                         }
    00367                 }
    00368                 else if (stream.peek() != 'h')
    00369                 {
    00370                         print_ISAT_shell_help('c');
    00371                 }
    00372                 else
    00373                 {
    00374                         cout << "Invalid command." << endl;
    00375                         cout << "\tc [OPTION] [NUMBER]" << endl;
    00376                 }
    00377         }
    00378         else
    00379         {
    00380                 cout << "Invalid command." << endl;
    00381                 cout << "\tc [OPTION] [NUMBER]" << endl;
    00382         }
    00383 }
    00384
    00385 void
    00386 run_d_command(istream & stream)
    00387 {
    00388         eat_space_or_tab(stream);
    00389         switch (stream.peek())
    00390         {
    00391         case '\n':
    00392                 if (use_DPLL)
    00393                 {
    00394                         use_DPLL = false;
    00395                         cout << "DPLL is off." << endl;
    00396                 }
    00397                 else
    00398                 {
    00399                         use_DPLL = true;
    00400                         cout << "DPLL is on." << endl;
    00401
    00402                 }
    00403                 break;
    00404         case '-':
    00405                 stream.ignore(1);
    00406                 switch (stream.peek())
    00407                 {
    00408                 case 'h':
    00409                         print_ISAT_shell_help('d');
    00410                         break;
    00411                 default:
    00412                         cout << "Invalid command." << endl;
    00413                         cout << "\td" << endl;
    00414                 }
    00415                 break;
    00416         default:
    00417                 cout << "Invalid command." << endl;
    00418                 cout << "\td" << endl;
    00419                 break;
    00420         }
    00421 }
    00422
    00423 void
    00424 run_f_command(istream & stream)
    00425 {
    00426         unsigned int            i;
    00427         char    char_array[300];
    00428         string  temp_string;
    00429         eat_space_or_tab(stream);
    00430         if (stream.peek() == '\n')
    00431         {
    00432                 print_facts();
    00433         }
    00434         else if (stream.peek() == '-')
    00435         {
    00436                 stream.ignore(1);
    00437                 stream.get(char_array, 2);
    00438                 eat_space_or_tab(stream);
    00439                 if (stream.peek() >= '0' && stream.peek() <= '9')
    00440                 {
    00441                         stream >> i;
    00442                         if (i < clauses.size())
    00443                         {
    00444                                 switch (char_array[0])
    00445                                 {
    00446                                 case 'i':
    00447                                 case 'I':
    00448                                         set_fact(i, true);
    00449                                         break;
    00450                                 case 'r':
    00451                                 case 'R':
    00452                                         set_fact(i, false);
    00453                                         break;
    00454                                 default:
    00455                                         cout << "Invalid command." << endl;
    00456                                         cout << "\tf [OPTION] [NUMBER]" << endl;
    00457                                         break;
    00458                                 }
    00459                         }
    00460                         else
    00461                         {
    00462                                 cout << "Invalid clause index (0-" << clauses.size()-1 << ")." << endl;
    00463                         }
    00464                 }
    00465                 else if (char_array[0] == 'r' || char_array[0] == 'R')
    00466                 {
    00467                         temp_string = "";
    00468                         while (temp_string != "yes" && temp_string != "no")
    00469                         {
    00470                                 cout << "Would you like to remove all clauses from facts? [yes/no] ";
    00471                                 stream >> temp_string;
    00472                         }
    00473                         if (temp_string == "yes")
    00474                         {
    00475                                 for (i = 0; i < isFactClause.size(); i++)
    00476                                 {
    00477                                         isFactClause[i] = false;
    00478                                 }
    00479                         }
    00480                 }
    00481                 else if (stream.peek() != 'h')
    00482                 {
    00483                         print_ISAT_shell_help('f');
    00484                 }
    00485                 else
    00486                 {
    00487                         cout << "Invalid command." << endl;
    00488                         cout << "\tf [OPTION] [NUMBER]" << endl;
    00489                 }
    00490         }
    00491         else
    00492         {
    00493                 cout << "Invalid command." << endl;
    00494                 cout << "\tf [OPTION] [NUMBER]" << endl;
    00495         }
    00496 }
    00497
    00498 void
    00499 run_h_command(istream & stream)
    00500 {
    00501         char    char_array[300];
    00502         eat_space_or_tab(stream);
    00503         switch (stream.peek())
    00504         {
    00505         case '\n':
    00506                 print_ISAT_shell_help('h');
    00507                 cout << endl;
    00508                 break;
    00509         case '-':
    00510                 stream.ignore();
    00511                 stream.get(char_array, 2);
    00512                 print_ISAT_shell_help(char_array[0]);
    00513                 cout << endl;
    00514                 break;
    00515         default:
    00516                 cout << "Invalid command." << endl;
    00517                 print_ISAT_shell_help('h');
    00518                 cout << endl;
    00519                 break;
    00520         }
    00521 }
    00522
    00523 void
    00524 run_i_command(istream & stream)
    00525 {
    00526         eat_space_or_tab(stream);
    00527         switch (stream.peek())
    00528         {
    00529         case '\n':
    00530                 print_clause_index();
    00531                 break;
    00532         case '-':
    00533                 stream.ignore(1);
    00534                 switch (stream.peek())
    00535                 {
    00536                 case 'h':
    00537                         print_ISAT_shell_help('i');
    00538                         break;
    00539                 default:
    00540                         cout << "Invalid command." << endl;
    00541                         cout << "\ti" << endl;
    00542                 }
    00543                 break;
    00544                 default:
    00545                         cout << "Invalid command." << endl;
    00546                         cout << "\ti" << endl;
    00547                         break;
    00548         }
    00549 }
    00550
    00551 void
    00552 run_l_command(istream & stream)
    00553 {
    00554         string temp_string;
    00555         eat_space_or_tab(stream);
    00556         switch (stream.peek())
    00557         {
    00558         case '\n':
    00559                 cout << "Invalid command." << endl;
    00560                 cout << "\tl [OPTION] [FILE NAME]" << endl;
    00561                 break;
    00562         case '-':
    00563                 stream.ignore(1);
    00564                 switch (stream.peek())
    00565                 {
    00566                 case 'h':
    00567                 case 'H':
    00568                         print_ISAT_shell_help('l');
    00569                         break;
    00570                 case 'd':
    00571                 case 'D':
    00572                         stream.ignore(1);
    00573                         eat_space_or_tab(stream);
    00574                         stream >> temp_string;
    00575                         load_DIMACS_file(&temp_string);
    00576                         break;
    00577                 case 'm':
    00578                 case 'M':
    00579                         stream.ignore(1);
    00580                         eat_space_or_tab(stream);
    00581                         stream >> temp_string;
    00582                         load_MOF_file(&temp_string);
    00583                         break;
    00584                 case 's':
    00585                 case 'S':
    00586                         stream.ignore(1);
    00587                         eat_space_or_tab(stream);
    00588                         stream >> temp_string;
    00589                         load_script_file(&temp_string);
    00590                         break;
    00591                 default:
    00592                         cout << "Invalid command." << endl;
    00593                         cout << "\tl [OPTION] [FILE NAME]" << endl;
    00594                         break;
    00595                 }
    00596                 break;
    00597         default:
    00598                 cout << "Invalid command." << endl;
    00599                 cout << "\tl [OPTION] [FILE NAME]" << endl;
    00600                 break;
    00601         }
    00602 }
    00603
    00604 void
    00605 run_n_command(istream & stream)
    00606 {
    00607         eat_space_or_tab(stream);
    00608         switch (stream.peek())
    00609         {
    00610         case '\n':
    00611                 cout << "Invalid command." << endl;
    00612                 cout << "\tn [OPTION]" << endl;
    00613                 break;
    00614         case '-':
    00615                 stream.ignore(1);
    00616                 switch (stream.peek())
    00617                 {
    00618                 case 'h':
    00619                 case 'H':
    00620                         print_ISAT_shell_help('n');
    00621                         break;
    00622                 case 'c':
    00623                 case 'C':
    00624                         print_counters();
    00625                         break;
    00626                 case 'r':
    00627                 case 'R':
    00628                         reset_time_and_counters();
    00629                         break;
    00630                 case 't':
    00631                 case 'T':
    00632                         print_time();
    00633                         break;
    00634                 default:
    00635                         cout << "Invalid command." << endl;
    00636                         cout << "\tn [OPTION]" << endl;
    00637                         break;
    00638                 }
    00639                 break;
    00640         default:
    00641                 cout << "Invalid command." << endl;
    00642                 cout << "\tn [OPTION]" << endl;
    00643                 break;
    00644         }
    00645 }
    00646
    00647 void
    00648 run_p_command(istream & stream)
    00649 {
    00650         eat_space_or_tab(stream);
    00651         switch (stream.peek())
    00652         {
    00653         case '\n':
    00654                 SAT_engine.propagate_clauses(use_DPLL);
    00655                 break;
    00656         case '-':
    00657                 stream.ignore(1);
    00658                 switch (stream.peek())
    00659                 {
    00660                 case 'h':
    00661                 case 'H':
    00662                         print_ISAT_shell_help('p');
    00663                         break;
    00664                 default:
    00665                         cout << "Invalid command." << endl;
    00666                         cout << "\tn [OPTION]" << endl;
    00667                         break;
    00668                 }
    00669                 break;
    00670         default:
    00671                 cout << "Invalid command." << endl;
    00672                 cout << "\tp" << endl;
    00673                 break;
    00674         }
    00675 }
    00676
    00677 void
    00678 run_q_command(istream & stream)
    00679 {
    00680         eat_space_or_tab(stream);
    00681         switch (stream.peek())
    00682         {
    00683         case '\n':
    00684                 quit_shell = true;
    00685                 break;
    00686         case '-':
    00687                 stream.ignore(1);
    00688                 switch (stream.peek())
    00689                 {
    00690                 case 'h':
    00691                         print_ISAT_shell_help('q');
    00692                         break;
    00693                 default:
    00694                         cout << "Invalid command." << endl;
    00695                         cout << "\tq" << endl;
    00696                 }
    00697                 break;
    00698         default:
    00699                 cout << "Invalid command." << endl;
    00700                 cout << "\tq" << endl;
    00701                 break;
    00702         }
    00703 }
    00704
    00705 void
    00706 run_t_command(istream & stream)
    00707 {
    00708         char    char_array[300];
    00709         eat_space_or_tab(stream);
    00710         switch (stream.peek())
    00711         {
    00712         case '\n':
    00713                 cout << "Invalid command." << endl;
    00714                 cout << "\tt [OPTION]" << endl;
    00715                 break;
    00716         case '-':
    00717                 stream.ignore();
    00718                 if (stream.peek() == 'h')
    00719                 {
    00720                         print_ISAT_shell_help('t');
    00721                 }
    00722                 else
    00723                 {
    00724                         stream.get(char_array, 2);
    00725                         print_theory_info(char_array[0]);
    00726                 }
    00727                 break;
    00728         default:
    00729                 cout << "Invalid command." << endl;
    00730                 cout << "\tt [OPTION]" << endl;
    00731         }
    00732 }
    00733
    00734 void
    00735 print_ISAT_shell_help(char ch)
    00736 {
    00737         switch (ch)
    00738         {
    00739 #if defined(_DEBUG)
    00740         // 'b' or 'B' corresponds to debug level.
    00741         case 'b':
    00742         case 'B':
    00743                 cout << "NAME" << endl;
    00744                 cout << "\tb - set debug level" << endl;
    00745                 cout << endl;
    00746                 cout << "SYNOPSIS" << endl;
    00747                 cout << "\tb [NUMBER]" << endl;
    00748                 cout << endl;
    00749                 cout << "DESCRIPTION" << endl;
    00750                 cout << "\tSets the debug level. Zero corresponds to debug off and" << endl;
    00751                 cout << "\tgreater number will display more debug information." << endl;
    00752                 cout << endl;
    00753                 break;
    00754 #endif // #if defined(_DEBUG)
    00755         // 'c' or 'C' corresponds to clause.
    00756         case 'c':
    00757         case 'C':
    00758                 cout << "NAME" << endl;
    00759                 cout << "\tc - displays or modifies a clause" << endl;
    00760                 cout << endl;
    00761                 cout << "SYNOPSIS" << endl;
    00762                 cout << "\tc [OPTION] [NUMBER]" << endl;
    00763                 cout << endl;
    00764                 cout << "DESCRIPTION" << endl;
    00765                 cout << "\tDisplays information of the clause corresponding to the" << endl;
    00766                 cout << "\tprovided index. When no option is provided, it displays a" << endl;
    00767                 cout << "\tdefault clause information." << endl;
    00768                 cout << endl;
    00769                 cout << "\t-a\tactivate the clause." << endl;
    00770                 cout << "\t-d\tdeactivate the clause." << endl;
    00771                 cout << "\t-r\tremove the clause." << endl;
    00772                 cout << endl;
    00773                 break;;
    00774         // 'd' or 'D' corresponds to toggle DPLL on or off.
    00775         case 'd':
    00776         case 'D':
    00777                 cout << "NAME" << endl;
    00778                 cout << "\td - toggle using DPLL" << endl;
    00779                 cout << endl;
    00780                 cout << "SYNOPSIS" << endl;
    00781                 cout << "\td" << endl;
    00782                 cout << endl;
    00783                 cout << "DESCRIPTION" << endl;
    00784                 cout << "\tToggle using DPLL true or false." << endl;
    00785                 cout << endl;
    00786                 break;
    00787                 // 'c' or 'C' corresponds to clause.
    00788
    00789         case 'f':
    00790         case 'F':
    00791                 cout << "NAME" << endl;
    00792                 cout << "\tf - displays or modifies fact clauses" << endl;
    00793                 cout << endl;
    00794                 cout << "SYNOPSIS" << endl;
    00795                 cout << "\tf [OPTION] [NUMBER]" << endl;
    00796                 cout << endl;
    00797                 cout << "DESCRIPTION" << endl;
    00798                 cout << "\tEither adds or removes a clause with the provided index" << endl;
    00799                 cout << "\tfrom facts. When no option is provided, it displays the" << endl;
    00800                 cout << "\tof fact clauses." << endl;
    00801                 cout << endl;
    00802                 cout << "\t-i\tinserts the clause into facts." << endl;
    00803                 cout << "\t-r\tremoves the clause from facts. If no index is given," << endl;
    00804                 cout << "\t  \tall fact clauses are removed from facts." << endl;
    00805                 cout << endl;
    00806                 break;
    00807         // 'i' or 'I' corresponds to clause index.
    00808         case 'i':
    00809         case 'I':
    00810                 cout << "NAME" << endl;
    00811                 cout << "\ti - displays all clauses and their corresponding indicies" << endl;
    00812                 cout << endl;
    00813                 cout << "SYNOPSIS" << endl;
    00814                 cout << "\ti" << endl;
    00815                 cout << "DESCRIPTION" << endl;
    00816                 cout << "\tDisplays all clauses and their corresponding indicies." << endl;
    00817                 cout << endl;
    00818                 break;
    00819                 // 'i' or 'I' corresponds to clause index.
    00820         case 'l':
    00821         case 'L':
    00822                 cout << "NAME" << endl;
    00823                 cout << "\tl - load theory from file" << endl;
    00824                 cout << endl;
    00825                 cout << "SYNOPSIS" << endl;
    00826                 cout << "\tl [OPTION] [FILE NAME]" << endl;
    00827                 cout << "DESCRIPTION" << endl;
    00828                 cout << "\tLoad theory from file. The file type can be specified" << endl;
    00829                 cout << "\tby using the option." << endl;
    00830                 cout << endl;
    00831                 cout << "\t-d\tDIMACS file" << endl;
    00832                 cout << "\t-m\tMOF file" << endl;
    00833                 cout << "\t-s\tscript file" << endl;
    00834                 cout << endl;
    00835                 break;
    00836         // 'n' or 'N' corresponds to the number of times
    00837         case 'n':
    00838         case 'N':
    00839                 cout << "NAME" << endl;
    00840                 cout << "\tn - displays timing information" << endl;
    00841                 cout << endl;
    00842                 cout << "SYNOPSIS" << endl;
    00843                 cout << "\tn [OPTION]" << endl;
    00844                 cout << endl;
    00845                 cout << "DESCRIPTION" << endl;
    00846                 cout << "\tDisplays the values corresponding to the option." << endl;
    00847                 cout << endl;
    00848                 cout << "\t-r\treset propagation and time counters" << endl;
    00849                 cout << "\t-c\tdisplays the number of times propositions are assigned" << endl;
    00850                 cout << "\t\tand unassigned since last reset" << endl;
    00851                 cout << "\t-t\tdisplays the time it took to propagate all changes" << endl;
    00852                 cout << "\t\tsince last reset" << endl;
    00853                 cout << endl;
    00854                 break;
    00855         // 'p' or 'P' corresponds to propagate
    00856         case 'p':
    00857         case 'P':
    00858                 cout << "NAME" << endl;
    00859                 cout << "\tp - propagate" << endl;
    00860                 cout << endl;
    00861                 cout << "SYNOPSIS" << endl;
    00862                 cout << "\tp" << endl;
    00863                 cout << endl;
    00864                 cout << "DESCRIPTION" << endl;
    00865                 cout << "\tpropagates all changes (add and remove clauses)" << endl;
    00866                 cout << "\tmade since last propagation." << endl;
    00867                 break;
    00868         // 'q' or 'Q' corresponds to quit.
    00869         case 'q':
    00870         case 'Q':
    00871                 cout << "NAME" << endl;
    00872                 cout << "\tq - quit ISAT shell" << endl;
    00873                 cout << endl;
    00874                 cout << "SYNOPSIS" << endl;
    00875                 cout << "\tq" << endl;
    00876                 cout << endl;
    00877                 cout << "DESCRIPTION" << endl;
    00878                 cout << "\tQuits out of ISAT shell." << endl;
    00879                 cout << endl;
    00880                 break;
    00881         // 't' or 'T' corresponds to theory information.
    00882         case 't':
    00883         case 'T':
    00884                 cout << "NAME" << endl;
    00885                 cout << "\tt - displays theory information" << endl;
    00886                 cout << endl;
    00887                 cout << "SYNOPSIS" << endl;
    00888                 cout << "\tt [OPTION]" << endl;
    00889                 cout << endl;
    00890                 cout << "DESCRIPTION" << endl;
    00891                 cout << "\tDisplays the theory information corresponding to the option." << endl;
    00892                 cout << endl;
    00893                 cout << "\t-c\tdisplays the consistency of the theory." << endl;
    00894                 cout << "\t-i\tdisplays inconsistent clauses." << endl;
    00895                 cout << "\t-p\tdisplays all propositions and their truth values." << endl;
    00896                 cout << "\t-s\tdisplays SAT conflicts." << endl;
    00897                 cout << "\t-u\tdisplays UNSAT conflicts." << endl;
    00898                 cout << endl;
    00899                 break;
    00900         // 'h', 'H', or '?' corresponds to help menu.
    00901         default:
    00902                 cout << "---------------------------------------------------------------" << endl;
    00903                 cout << "ISAT Shell" << endl;
    00904                 cout << "---------------------------------------------------------------" << endl;
    00905                 cout << "  Any of the commands followed by \"-h\" will display" << endl;
    00906                 cout << "  additional help info." << endl;
    00907                 cout << endl;
    00908 #if defined(_DEBUG)
    00909                 cout << "  b : set debug level" << endl;
    00910 #endif // #if defined(_DEBUG)
    00911                 cout << "  c : display/modify clause" << endl;
    00912                 cout << "  d : toggle DPLL usage" << endl;
    00913                 cout << "  f : display/modify facts" << endl;
    00914                 cout << "  h : displays this help" << endl;
    00915                 cout << "  i : displays all clauses and their indicies" << endl;
    00916                 cout << "  l : load theory from a file" << endl;
    00917                 cout << "  n : displays/resets timing information" << endl;
    00918                 cout << "  p : propagate" << endl;
    00919                 cout << "  q : quit" << endl;
    00920                 cout << "  t : displays theory information" << endl;
    00921                 cout << "  # : comment line" << endl;
    00922                 cout << endl;
    00923                 break;
    00924         }
    00925 }
    00926
    00927 void
    00928 print_theory_info(char ch)
    00929 {
    00930         ISATTheory::ConsistencyType consistency = SAT_engine.get_consistency(use_DPLL);
    00931
    00932         switch (ch)
    00933         {
    00934         case 'c':
    00935         case 'C':
    00936                 //consistency = SAT_engine.get_consistency(use_DPLL);
    00937                 cout << "Theory is " << consistency << "." << endl;
    00938                 break;
    00939         case 'i':
    00940         case 'I':
    00941                 cout << "Inconsistent Clauses:" << endl;
    00942                 cout << *SAT_engine.get_inconsistent_clauses_p() << endl;
    00943                 break;
    00944         case 'p':
    00945         case 'P':
    00946                 cout << "Propositions:" << endl;
    00947                 cout << *SAT_engine.get_propositions_p() << endl;
    00948                 break;
    00949         case 's':
    00950         case 'S':
    00951                 cout << "SAT Conflicts:" << endl;
    00952                 //cout << facts.is_empty() ? *SAT_engine.get_SAT_conflicts_p(use_DPLL) : *SAT_engine.get_SAT_conflicts_p_using_fact(use_DPLL, &facts) << endl;
    00953                 cout << (facts.is_empty() ? *SAT_engine.get_SAT_conflicts_p(use_DPLL) : *SAT_engine.get_SAT_conflicts_p_using_fact(use_DPLL, &facts)) << endl;
    00954                 break;
    00955         case 'u':
    00956         case 'U':
    00957                 cout << "UNSAT Conflicts:" << endl;
    00958                 cout << (facts.is_empty() ? *SAT_engine.get_UNSAT_conflicts_p(use_DPLL) : *SAT_engine.get_UNSAT_conflicts_p_using_fact(use_DPLL, &facts)) << endl;
    00959                 break;
    00960         default:
    00961                 cout << "Invalid command." << endl;
    00962                 print_ISAT_shell_help('t');
    00963                 cout << endl;
    00964                 break;
    00965         }
    00966 }
    00967
    00968 void
    00969 print_clause_index()
    00970 {
    00971         ISATClause *clause_p;
    00972         for (unsigned int i = 0; i < clauses.size(); i++)
    00973         {
    00974                 clause_p = clauses[i];
    00975                 cout << "[" << i << "] " << *clause_p << " [" << clause_p->get_consistency()
    00976                          << "]";
    00977                 if (clause_p->is_active())
    00978                 {
    00979                         cout << " <-- ACTIVE";
    00980                 }
    00981                 else
    00982                 {
    00983                         cout << " <-- INACTIVE";
    00984                 }
    00985                 if (isFactClause[i])
    00986                 {
    00987                         cout << " [FACT]" << endl;
    00988                 }
    00989                 else
    00990                 {
    00991                         cout << endl;
    00992                 }
    00993         }
    00994 }
    00995
    00996 void
    00997 print_clause(unsigned int i)
    00998 {
    00999         if (i < clauses.size())
    01000         {
    01001                 ISATClause *clause_p = clauses[i];
    01002                 cout << "[" << i << "] " << *clause_p << " [" << clause_p->get_consistency()
    01003                          << "]";
    01004                 if (clause_p->is_active())
    01005                 {
    01006                         cout << " <-- ACTIVE";
    01007                         if (isFactClause[i])
    01008                         {
    01009                                 cout << "[FACT]" << endl;
    01010                         }
    01011                         else
    01012                         {
    01013                                 cout << endl;
    01014                         }
    01015                         if (clause_p->is_consistent())
    01016                         {
    01017                                 cout << "\tClause is consistent because ("
    01018                                          << *clause_p->get_satisfying_literal_p()->get_proposition_p()
    01019                                          << ")." << endl;
    01020                         }
    01021                 }
    01022                 else
    01023                 {
    01024                         cout << " <-- INACTIVE"<< endl;
    01025                 }
    01026         }
    01027         else
    01028         {
    01029                 cout << "Invalid clause index (0-" << clauses.size()-1 << ")." << endl;
    01030         }
    01031 }
    01032
    01033 void
    01034 print_facts()
    01035 {
    01036         ISATClause *clause_p;
    01037         for (unsigned int i = 0; i < clauses.size(); i++)
    01038         {
    01039                 if (isFactClause[i])
    01040                 {
    01041                         clause_p = clauses[i];
    01042                         cout << "[" << i << "] " << *clause_p << " [" << clause_p->get_consistency()
    01043                                 << "]";
    01044                         if (clause_p->is_active())
    01045                         {
    01046                                 cout << " <-- ACTIVE" << endl;
    01047                         }
    01048                         else
    01049                         {
    01050                                 cout << " <-- INACTIVE" << endl;
    01051                         }
    01052                 }
    01053         }
    01054 }
    01055
    01056 void print_counters()
    01057 {
    01058         cout << "# of proposition assignment: ";
    01059         cout << SAT_engine.get_assign_proposition_counter();
    01060         cout << endl;
    01061
    01062         cout << "# of proposition unassignment: ";
    01063         cout << SAT_engine.get_unassign_proposition_counter();
    01064         cout << endl;
    01065
    01066         return;
    01067 }
    01068
    01069 void print_time()
    01070 {
    01071         cout << "total time (s): ";
    01072         cout << SAT_engine.get_total_time();
    01073         cout << endl;
    01074
    01075         return;
    01076 }
    01077
    01078 void reset_time_and_counters()
    01079 {
    01080         SAT_engine.reset_time_and_counters();
    01081         return;
    01082 }
    01083
    01084 void
    01085 activate_clause(unsigned int i)
    01086 {
    01087         if (i < clauses.size())
    01088         {
    01089                 SAT_engine.activate_clause(clauses[i]);
    01090
    01091                 print_clause(i);
    01092                 cout << endl;
    01093         }
    01094         else
    01095         {
    01096                 cout << "Invalid clause index (0-" << clauses.size()-1 << ")." << endl;
    01097         }
    01098 }
    01099
    01100 void
    01101 deactivate_clause(unsigned int i)
    01102 {
    01103         if (i < clauses.size())
    01104         {
    01105                 SAT_engine.deactivate_clause(clauses[i]);
    01106
    01107                 print_clause(i);
    01108                 cout << endl;
    01109         }
    01110         else
    01111         {
    01112                 cout << "Invalid clause index (0-" << clauses.size()-1 << ")." << endl;
    01113         }
    01114 }
    01115
    01116 void
    01117 remove_clause(unsigned int i)
    01118 {
    01119         if (i < clauses.size())
    01120         {
    01121                 ISATClause *clause_p = clauses[i];
    01122                 cout << "Removing " << *clause_p << "." << endl;
    01123                 vector<ISATClause *>::iterator clauses_iter = clauses.begin();
    01124                 vector<bool>::iterator isFactClause_iter = isFactClause.begin();
    01125                 set_fact(i, false);
    01126                 clauses.erase(clauses_iter + i);
    01127                 isFactClause.erase(isFactClause_iter + i);
    01128                 SAT_engine.remove_clause(clause_p);
    01129         }
    01130         else
    01131         {
    01132                 cout << "Invalid clause index (0-" << clauses.size()-1 << ")." << endl;
    01133         }
    01134 }
    01135
    01136 void
    01137 set_fact(unsigned int i, bool isFact)
    01138 {
    01139         if (i < isFactClause.size())
    01140         {
    01141                 bool wasFact = isFactClause[i];
    01142                 if (wasFact && !isFact)
    01143                 {
    01144                         facts.remove_clause(clauses[i]);
    01145                 }
    01146                 else if (!wasFact && isFact)
    01147                 {
    01148                         facts.insert_clause(clauses[i]);
    01149                 }
    01150                 isFactClause[i] = isFact;
    01151         }
    01152 }
    01153
    01154 void
    01155 eat_space_or_tab(istream &stream)
    01156 {
    01157         while(stream.peek() == ' ' || stream.peek() == '\t')
    01158         {
    01159                 stream.ignore(1);
    01160         }
    01161 }
    01162
    01163 void
    01164 clear_stream(istream &stream)
    01165 {
    01166         while (stream.peek() != '\n' && !stream.eof())
    01167         {
    01168                 stream.ignore(1);
    01169         }
    01170         stream.ignore(1);
    01171 }
    01172
    01173 void
    01174 load_DIMACS_file(string const *file_name_p)
    01175 {
    01176         ifstream        DIMACS_stream;
    01177         bool            is_cnf_format = true;
    01178         int                     numb_of_propositions;
    01179         int                     numb_of_clauses;
    01180         int                     stream_length;
    01181         char            temp_char_array[500];
    01182         string          temp_string;
    01183
    01184         DIMACS_stream.open(file_name_p->c_str());
    01185
    01186         // Make sure the File Exists
    01187         if (DIMACS_stream.bad())
    01188         {
    01189                 cerr << "File " << file_name_p << " does not exist." << endl;
    01190                 return;
    01191         }
    01192
    01193         // get length of file:
    01194         DIMACS_stream.seekg(0,ios::end);
    01195         stream_length = DIMACS_stream.tellg();
    01196         DIMACS_stream.seekg(0, ios::beg);
    01197
    01198
    01199         // Skip Comment Lines: c Comments
    01200         while (DIMACS_stream.peek() == 'c' && !DIMACS_stream.eof())
    01201         {
    01202                 DIMACS_stream.getline(temp_char_array, stream_length, '\n');
    01203                 cout << temp_char_array << endl;
    01204         }
    01205
    01206         // Read in Problem Line: p FORMAT VARIABLES CLAUSES
    01207         if (DIMACS_stream.peek() == 'p')
    01208         {
    01209                 // Skip p
    01210                 DIMACS_stream.ignore(stream_length, 'p');
    01211                 // Read FORMAT
    01212                 DIMACS_stream >> temp_string;
    01213                 if (temp_string == "sat")
    01214                 {
    01215                         is_cnf_format = false;
    01216                 }
    01217                 else if (temp_string != "cnf")
    01218                 {
    01219                         cerr << "Error: Could not read problem format." << std::endl;
    01220                         return;
    01221                 }
    01222
    01223                 // Read VARIABLES
    01224                 DIMACS_stream >> numb_of_propositions;
    01225                 // Read CLAUSES
    01226                 DIMACS_stream >> numb_of_clauses;
    01227         }
    01228         else
    01229         {
    01230                 cerr << "Error: " << *file_name_p << " does not have a problem line." << endl;
    01231                 return;
    01232         }
    01233
    01234         cout << "\rReading file " << *file_name_p << " with " << numb_of_propositions
    01235                  << " propositions and " << numb_of_clauses << " clauses... ";
    01236         // Should include memory management.
    01237         if (is_cnf_format)
    01238         {
    01239                 load_DIMACS_CNF_format(DIMACS_stream);
    01240         }
    01241         else
    01242         {
    01243                 load_DIMACS_SAT_format(DIMACS_stream);
    01244         }
    01245         DIMACS_stream.close();
    01246         cout << "Done." << endl;
    01247 }
    01248
    01249 void
    01250 load_DIMACS_CNF_format(ifstream &DIMACS_stream)
    01251 {
    01252         ISATStringDescription * prop_desc_p;
    01253         ISATClause *                    clause_p;
    01254         string                                  temp_string;
    01255
    01256         clause_p = SAT_engine.insert_new_empty_clause();
    01257
    01258         // Read in All Clauses
    01259         while (!DIMACS_stream.eof())
    01260         {
    01261                 // Read in a literal
    01262                 DIMACS_stream >> temp_string;
    01263
    01264                 // Check if Literal signals end of the clause
    01265                 if (temp_string == "0" && clause_p->get_numb_of_literals() > 0)
    01266                 {
    01267                         SAT_engine.activate_clause(clause_p);
    01268                         clauses.push_back(clause_p);
    01269                         isFactClause.push_back(false);
    01270                         clause_p = SAT_engine.insert_new_empty_clause();
    01271                 }
    01272
    01273                 //added to temp_string != "0"
    01274                 //otherwise a proposition named "0" ends up in the list of propositions
    01275                 //but no such proposition can exist since 0 marks end of line in dimacs files
    01276                 else if (temp_string != "0" && temp_string != "")
    01277                 {
    01278                         if (*temp_string.begin() == '-')
    01279                         {
    01280                                 temp_string.erase(0,1);
    01281                                 assert(temp_string != "");
    01282                                 prop_desc_p = new ISATStringDescription(&temp_string);
    01283                                 SAT_engine.add_literal_to_new_clause(prop_desc_p, ISATLiteral::NEGATIVE);
    01284                         }
    01285                         else
    01286                         {
    01287                                 assert(temp_string != "");
    01288                                 prop_desc_p = new ISATStringDescription(&temp_string);
    01289                                 SAT_engine.add_literal_to_new_clause(prop_desc_p, ISATLiteral::POSITIVE);
    01290                         }
    01291                 }
    01292         }
    01293 }
    01294
    01295
    01296 void
    01297 load_MOF_file(string const *file_name_p)
    01298 {
    01299         CCAModel                                new_model;
    01300         CCASentence                             new_sentence(true, CCASentence::CNF);
    01301         string                                  temp_string;
    01302         ISATStringDescription * prop_desc_p;
    01303         ISATClause *                    clause_p;
    01304
    01305         cout << "\rReading file " << *file_name_p << "... ";
    01306
    01307         if(MOFReader:: loadMOF(file_name_p->c_str(), new_model))
    01308         {
    01309                 cout << endl;
    01310                 cerr << "File " << *file_name_p << " does not exist." << endl;
    01311                 return;
    01312         }
    01313         else
    01314         {
    01315                 new_sentence = new_model.get_all_constraints();
    01316                 for (CCASentence::const_iterator s_const_it = new_sentence.begin();
    01317                 s_const_it != new_sentence.end(); s_const_it++)
    01318                 {
    01319                         clause_p = SAT_engine.insert_new_empty_clause();
    01320                         for (CCAClause::const_iterator c_const_it = (*s_const_it).begin();
    01321                         c_const_it != (*s_const_it).end(); c_const_it++)
    01322                         {
    01323                                 temp_string = (*c_const_it).getVariable()->getName();
    01324                                 temp_string = temp_string + "=";
    01325                                 temp_string = temp_string + (*c_const_it).getValue()->getName();
    01326                                 prop_desc_p = new ISATStringDescription(&temp_string);
    01327                                 if ((*c_const_it).getOperator() == CCAAssignment::Positive)
    01328                                 {
    01329                                         SAT_engine.add_literal_to_new_clause(
    01330                                                 prop_desc_p, ISATLiteral::POSITIVE);
    01331                                 }
    01332                                 else
    01333                                 {
    01334                                         SAT_engine.add_literal_to_new_clause(
    01335                                                 prop_desc_p, ISATLiteral::NEGATIVE);
    01336                                 }
    01337                         }
    01338                         SAT_engine.activate_clause(clause_p);
    01339                         clauses.push_back(clause_p);
    01340                         isFactClause.push_back(false);
    01341                 }
    01342                 cout << "Done." << endl;
    01343         }
    01344 }
    01345
    01346 void
    01347 load_script_file(string const *file_name_p)
    01348 {
    01349         ifstream        script_stream;
    01350         int                     stream_length;
    01351         string          temp_string;
    01352
    01353         script_stream.open(file_name_p->c_str());
    01354
    01355         // Make sure the File Exists
    01356         if (script_stream.bad())
    01357         {
    01358                 cerr << "File " << file_name_p << " does not exist." << endl;
    01359                 return;
    01360         }
    01361
    01362         cout << "\rReading file " << *file_name_p << "... " << endl;
    01363
    01364         // get length of file:
    01365         script_stream.seekg(0,ios::end);
    01366         stream_length = script_stream.tellg();
    01367         script_stream.seekg(0, ios::beg);
    01368
    01369         while (!quit_shell && !script_stream.eof())
    01370         {
    01371                 run_command(script_stream);
    01372         }
    01373         script_stream.close();
    01374         cout << "Done." << endl;
    01375 }