cprover
pbs_dimacs_cnf.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Alex Groce
6 
7 \*******************************************************************/
8 
9 #include "pbs_dimacs_cnf.h"
10 
11 #include <cstdlib>
12 #include <cstring>
13 #include <fstream>
14 
15 #ifdef DEBUG
16 #include <iostream>
17 #endif
18 
19 void pbs_dimacs_cnft::write_dimacs_pb(std::ostream &out)
20 {
21  double d_sum = 0;
22 
23 #ifdef DEBUG
24  std::cout << "enter: No Lit.=" << no_variables() << "\n";
25 #endif
26 
27  for(const auto &lit_entry : pb_constraintmap)
28  d_sum += lit_entry.second;
29 
30  if(!optimize)
31  {
32  out << "# PBType: E" << "\n";
33  out << "# PBGoal: " << goal << "\n";
34  }
35  else if(!maximize)
36  {
37  out << "# PBType: SE" << "\n";
38  out << "# PBGoal: " << d_sum << "\n";
39  out << "# PBObj : MIN" << "\n";
40  }
41  else
42  {
43  out << "# PBType: GE" << "\n";
44  out << "# PBGoal: " << 0 << "\n";
45  out << "# PBObj : MAX" << "\n";
46  }
47 
48  out << "# NumCoef: " << pb_constraintmap.size() << "\n";
49 
50  for(const auto &lit_entry : pb_constraintmap)
51  {
52  const int dimacs_lit = lit_entry.first.dimacs();
53  out << "v" << dimacs_lit << " c" << lit_entry.second << "\n";
54  }
55 
56 #ifdef DEBUG
57  std::cout << "exit: No Lit.=" << no_variables() << "\n";
58 #endif
59 }
60 
62 {
63 #ifdef DEBUG
64  std::cout << "solve: No Lit.=" << no_variables() << "\n";
65 #endif
66 
67  std::string command;
68 
69  if(!pbs_path.empty())
70  {
71  command += pbs_path;
72  if(command.substr(command.length(), 1) != "/")
73  command += "/";
74  }
75 
76  command += "pbs";
77 
78 #ifdef DEBUG
79  std::cout << "PBS COMMAND IS: " << command << "\n";
80 #endif
81 #if 0
82  if (!(getenv("PBS_PATH")==NULL))
83  {
84  command=getenv("PBS_PATH");
85  }
86  else
87  {
88  error ("Unable to read PBS_PATH environment variable.\n");
89  return false;
90  }
91 #endif
92 
93  command += " -f temp.cnf";
94 
95 #if 1
96  if(optimize)
97  {
98  if(binary_search)
99  {
100  command += " -S 1000 -D 1 -H -I -a";
101  }
102  else
103  {
104 #ifdef DEBUG
105  std::cout << "NO BINARY SEARCH"
106  << "\n";
107 #endif
108  command += " -S 1000 -D 1 -I -a";
109  }
110  }
111  else
112  {
113  command += " -S 1000 -D 1 -a";
114  }
115 #else
116  command += " -z";
117 #endif
118 
119  command += " -a > temp.out";
120 
121  const int res = system(command.c_str());
122  CHECK_RETURN(0 == res);
123 
124  std::ifstream file("temp.out");
125  std::string line;
126  int v;
127  bool satisfied = false;
128 
129  if(file.fail())
130  {
131  error() << "Unable to read SAT results!" << eom;
132  return false;
133  }
134 
135  opt_sum = -1;
136 
137  while(file && !file.eof())
138  {
139  std::getline(file, line);
140  if(
141  strstr(line.c_str(), "Variable Assignments Satisfying CNF Formula:") !=
142  nullptr)
143  {
144 #ifdef DEBUG
145  std::cout << "Reading assignments...\n";
146  std::cout << "No literals: " << no_variables() << "\n";
147 #endif
148  satisfied = true;
149  assigned.clear();
150  for(size_t i = 0; (file && (i < no_variables())); ++i)
151  {
152  file >> v;
153  if(v > 0)
154  {
155 #ifdef DEBUG
156  std::cout << v << " ";
157 #endif
158  assigned.insert(v);
159  }
160  }
161 #ifdef DEBUG
162  std::cout << "\n";
163  std::cout << "Finished reading assignments.\n";
164 #endif
165  }
166  else if(strstr(line.c_str(), "SAT... SUM") != nullptr)
167  {
168 #ifdef DEBUG
169  std::cout << line;
170 #endif
171  sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
172  }
173  else if(strstr(line.c_str(), "SAT - All implied") != nullptr)
174  {
175 #ifdef DEBUG
176  std::cout << line;
177 #endif
178  sscanf(
179  line.c_str(),
180  "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d",
181  &opt_sum);
182  }
183  else if(strstr(line.c_str(), "SAT... Solution") != nullptr)
184  {
185 #ifdef DEBUG
186  std::cout << line;
187 #endif
188  sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
189  }
190  else if(strstr(line.c_str(), "Optimal Soln") != nullptr)
191  {
192 #ifdef DEBUG
193  std::cout << line;
194 #endif
195  if(strstr(line.c_str(), "time out") != nullptr)
196  {
197  status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." << eom;
198  return satisfied;
199  }
200  sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
201  }
202  }
203 
204  return satisfied;
205 }
206 
208 {
209  std::ofstream file("temp.cnf");
210 
212 
213  std::ofstream pbfile("temp.cnf.pb");
214 
215  write_dimacs_pb(pbfile);
216 
217  file.close();
218  pbfile.close();
219 
220  // We start counting at 1, thus there is one variable fewer.
221  messaget::status() << (no_variables() - 1) << " variables, " << clauses.size()
222  << " clauses" << eom;
223 
224  const bool result = pbs_solve();
225 
226  if(!result)
227  {
228  messaget::status() << "PBS checker: system is UNSATISFIABLE" << eom;
229  }
230  else
231  {
232  messaget::status() << "PBS checker: system is SATISFIABLE";
233  if(optimize)
234  messaget::status() << " (distance " << opt_sum << ")";
235  messaget::status() << eom;
236  }
237 
238  if(result)
239  return resultt::P_SATISFIABLE;
240  else
242 }
243 
245 {
246  int dimacs_lit = a.dimacs();
247 
248 #ifdef DEBUG
249  std::cout << a << " / " << dimacs_lit << "=";
250 #endif
251 
252  const bool neg = (dimacs_lit < 0);
253  if(neg)
254  dimacs_lit = -dimacs_lit;
255 
256  std::set<int>::const_iterator f = assigned.find(dimacs_lit);
257 
258  if(!neg)
259  {
260  if(f == assigned.end())
261  {
262 #ifdef DEBUG
263  std::cout << "FALSE\n";
264 #endif
265  return tvt(false);
266  }
267  else
268  {
269 #ifdef DEBUG
270  std::cout << "TRUE\n";
271 #endif
272  return tvt(true);
273  }
274  }
275  else
276  {
277  if(f != assigned.end())
278  {
279 #ifdef DEBUG
280  std::cout << "FALSE\n";
281 #endif
282  return tvt(false);
283  }
284  else
285  {
286 #ifdef DEBUG
287  std::cout << "TRUE\n";
288 #endif
289  return tvt(true);
290  }
291  }
292 }
virtual tvt l_get(literalt a) const
std::string pbs_path
virtual resultt prop_solve()
int dimacs() const
Definition: literal.h:116
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
virtual void write_dimacs_pb(std::ostream &out)
virtual void write_dimacs_cnf(std::ostream &out)
Definition: dimacs_cnf.cpp:25
Definition: threeval.h:19
mstreamt & error() const
Definition: message.h:302
resultt
Definition: prop.h:96
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
literalt neg(literalt a)
Definition: literal.h:192
std::map< literalt, unsigned > pb_constraintmap
std::set< int > assigned
virtual size_t no_variables() const override
Definition: cnf.h:38
Definition: kdev_t.h:19