OKlibrary  0.2.1.6
FilterDimacs.cpp
Go to the documentation of this file.
00001 // Matthew Gwynne, 4.1.2011 (Swansea)
00002 /* Copyright 2011 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00056 #include <string>
00057 #include <fstream>
00058 #include <set>
00059 #include <iostream>
00060 #include <iterator>
00061 #include <algorithm>
00062 #include <functional>
00063 
00064 #include <boost/range/begin.hpp>
00065 #include <boost/range/end.hpp>
00066 #include <boost/range/algorithm.hpp>
00067 
00068 #include <OKlib/Satisfiability/Interfaces/InputOutput/Dimacs.hpp>
00069 #include <OKlib/Satisfiability/Interfaces/InputOutput/ClauseSetAdaptors.hpp>
00070 
00071 
00072 namespace OKlib {
00073   namespace InputOutput {
00074 
00075     template <typename Int = int, class String = std::string, 
00076               class CLSAdaptor = OKlib::InputOutput::CLSAdaptorDIMACSOutput<> >
00077     class CLSAdaptorFilter {
00078       
00079     public :
00080       
00081       typedef Int int_type;
00082       typedef String string_type;
00083       typedef CLSAdaptor cls_adaptor_type;
00084 
00085       typedef std::set<int_type> clause_index_container_type;
00086 
00087     private :
00088 
00089       cls_adaptor_type cls_adaptor;
00090       clause_index_container_type clause_index;
00091       int_type current_clause;
00092 
00093     public :
00094 
00095       template <typename Range>
00096       CLSAdaptorFilter(const Range& clause_index_arg, cls_adaptor_type& cls_adaptor_arg) : cls_adaptor(cls_adaptor_arg), current_clause(0) {
00097         boost::copy(clause_index_arg, 
00098                     std::inserter(clause_index, 
00099                                   boost::begin(clause_index)));
00100       }
00101  
00102       void comment(const string_type& s) { cls_adaptor.comment(s); }
00103       void n(const int_type pn) { cls_adaptor.n(pn); }
00104       void c(const int_type pc) {
00105         // Remove any clause-indices which are too large
00106         clause_index_container_type temp_clause_index;
00107         std::remove_copy_if(boost::begin(clause_index),
00108                             boost::end(clause_index),
00109                             std::inserter(temp_clause_index, 
00110                                           boost::begin(temp_clause_index)),
00111                             std::bind2nd(std::greater<int_type>(), pc));
00112         clause_index.clear();
00113         std::remove_copy_if(boost::begin(temp_clause_index),
00114                             boost::end(temp_clause_index),
00115                             std::inserter(clause_index, 
00116                                           boost::begin(clause_index)),
00117                             std::bind2nd(std::less<int_type>(), 1));
00118         
00119         cls_adaptor.c(clause_index.size());
00120       }
00121       void finish() { cls_adaptor.finish(); }
00122       void tautological_clause(const int_type t) {
00123         ++current_clause;
00124         if (clause_index.find(current_clause) != clause_index.end())
00125           cls_adaptor.tautological_clause(t);
00126       }
00127       template <class ForwardRange>
00128       void clause(const ForwardRange& r, const int_type t) {
00129         ++current_clause;
00130         if (clause_index.find(current_clause) != clause_index.end())
00131           cls_adaptor.clause(r,t);
00132       }
00133     };
00134   }
00135 }
00136 
00137 
00138 namespace {
00139 
00140   enum {
00141     error_parameters = 1,
00142     error_openfile = 2
00143   };
00144 
00145   const std::string program = "FilterDimacs";
00146   const std::string err = "ERROR[" + program + "]: ";
00147 
00148   const std::string version = "0.0.6";
00149 
00150 }
00151 
00152 int main(const int argc, const char* const argv[]) {
00153 
00154   if (argc != 2) {
00155     std::cerr << err << "Exactly one inputs is "
00156       "required, the  name of the file containing the list of "
00157       "clause positions. The Dimacs file should be given on standard input.\n";
00158     return error_parameters;
00159   }
00160 
00161   std::ifstream f_in(argv[1]);
00162   if (not f_in) {
00163     std::cerr << err << "Failure opening file " << argv[1] << ".\n";
00164     return error_openfile;
00165   }
00166 
00167   typedef OKlib::InputOutput::CLSAdaptorFilter<> CLSAdaptorFilter;
00168 
00169   CLSAdaptorFilter::clause_index_container_type clause_index;
00170   while (not f_in.eof()) {
00171     while ( (((char)f_in.peek() > '9') or 
00172             ((char)f_in.peek() < '0')) and
00173             ((char)f_in.peek() != '-') and 
00174             not f_in.eof()) {
00175       f_in.seekg(1,f_in.cur);
00176     }
00177     CLSAdaptorFilter::int_type i; 
00178     f_in >> i; 
00179     if (not f_in.fail() and (i > 0)) clause_index.insert(i);
00180   }
00181   f_in.close();
00182 
00183   CLSAdaptorFilter::cls_adaptor_type output(std::cout);
00184   CLSAdaptorFilter filter(clause_index, output);
00185   OKlib::InputOutput::StandardDIMACSInput<CLSAdaptorFilter>(std::cin, filter);
00186 }