cprover
read_dimacs_cnf.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Reading DIMACS CNF
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "read_dimacs_cnf.h"
13 
14 #include <istream>
15 #include <cstdlib> // for abs()
16 
17 #include <util/string2int.h>
18 
19 // #define VERBOSE
20 
21 void read_dimacs_cnf(std::istream &in, cnft &dest)
22 {
23  #define DELIMITERS "\t\n\v\f\r "
24  #define CHAR_DELIMITERS "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
25 
26  bvt new_bv;
27  std::string line;
28 
29  while(getline(in, line))
30  {
31  line += " ";
32 
33  while(true)
34  {
35  if(line.empty())
36  break;
37 
38  #ifdef VERBOSE
39  std::cout << "begin line " << line << '\n';
40  #endif
41  size_t pos = line.find_first_of(DELIMITERS, 0);
42  #ifdef VERBOSE
43  std::cout << "pos " << pos << '\n';
44  #endif
45  size_t pos_char = line.find_first_of(CHAR_DELIMITERS, 0);
46 
47  if(pos!=std::string::npos)
48  {
49  std::string decision = line.substr(0, pos);
50  line.erase(0, pos+1);
51  #ifdef VERBOSE
52  std::cout << "i am here\n";
53  std::cout << decision << '\n';
54  std::cout << "line" << line << '\n';
55  #endif
56  if(!decision.compare(std::string("c")))
57  {
58  #ifdef VERBOSE
59  std::cout << "c \n";
60  #endif
61  break;
62  }
63 
64  if(!decision.compare(std::string("p")))
65  {
66  #ifdef VERBOSE
67  std::cout << "p \n";
68  #endif
69  break;
70  }
71 
72  if(pos_char == std::string::npos) // no char present in the clause
73  {
74  int parsed_lit = unsafe_string2int(decision);
75  #ifdef VERBOSE
76  std::cout << "parsed_lit " << parsed_lit << " \n";
77  #endif
78  if(parsed_lit == 0)
79  {
80  bvt no_dup=cnft::eliminate_duplicates(new_bv);
81  #ifdef VERBOSE
82  std::cout << "calling lcnf " << new_bv.size() << '\n';
83  #endif
84  dest.lcnf(no_dup);
85  new_bv.clear();
86  no_dup.clear();
87  }
88  else
89  {
90  unsigned var = abs(parsed_lit); // because of the const variable
91  literalt l;
92  bool sign = (parsed_lit > 0) ? false : true;
93  l.set(var, sign);
94  #ifdef VERBOSE
95  std::cout << "setting l to " << l.get() << '\n';
96  #endif
97  new_bv.push_back(l);
98  if(dest.no_variables() <= var)
99  dest.set_no_variables(var+1);
100  }
101  }
102  }
103  }
104  }
105 }
void lcnf(literalt l0, literalt l1)
Definition: prop.h:53
static bvt eliminate_duplicates(const bvt &)
eliminate duplicates from given vector of literals
Definition: cnf.cpp:400
literalt pos(literalt a)
Definition: literal.h:193
var_not get() const
Definition: literal.h:102
#define CHAR_DELIMITERS
Definition: cnf.h:17
void set(var_not _l)
Definition: literal.h:92
virtual void set_no_variables(size_t no)
Definition: cnf.h:39
void read_dimacs_cnf(std::istream &in, cnft &dest)
Reading DIMACS CNF.
#define DELIMITERS
virtual size_t no_variables() const override
Definition: cnf.h:38
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
std::vector< literalt > bvt
Definition: literal.h:197