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