CBMC
Loading...
Searching...
No Matches
pbs_dimacs_cnf.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
19void 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 {
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 log.error() << "Unable to read SAT results!" << messaget::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 log.status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT."
198 << messaget::eom;
199 return satisfied;
200 }
201 sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
202 }
203 }
204
205 return satisfied;
206}
207
209{
210 PRECONDITION(assumptions.empty());
211
212 std::ofstream file("temp.cnf");
213
214 write_dimacs_cnf(file);
215
216 std::ofstream pbfile("temp.cnf.pb");
217
219
220 file.close();
221 pbfile.close();
222
223 // We start counting at 1, thus there is one variable fewer.
224 log.statistics() << (no_variables() - 1) << " variables, " << clauses.size()
225 << " clauses" << messaget::eom;
226
227 const bool result = pbs_solve();
228
229 if(!result)
230 {
231 log.status() << "PBS checker: system is UNSATISFIABLE" << messaget::eom;
232 }
233 else
234 {
235 log.status() << "PBS checker: system is SATISFIABLE";
236 if(optimize)
237 log.status() << " (distance " << opt_sum << ")";
239 }
240
241 if(result)
243 else
245}
246
248{
249 int dimacs_lit = a.dimacs();
250
251#ifdef DEBUG
252 std::cout << a << " / " << dimacs_lit << "=";
253#endif
254
255 const bool neg = (dimacs_lit < 0);
256 if(neg)
258
259 std::set<int>::const_iterator f = assigned.find(dimacs_lit);
260
261 if(!neg)
262 {
263 if(f == assigned.end())
264 {
265#ifdef DEBUG
266 std::cout << "FALSE\n";
267#endif
268 return tvt(false);
269 }
270 else
271 {
272#ifdef DEBUG
273 std::cout << "TRUE\n";
274#endif
275 return tvt(true);
276 }
277 }
278 else
279 {
280 if(f != assigned.end())
281 {
282#ifdef DEBUG
283 std::cout << "FALSE\n";
284#endif
285 return tvt(false);
286 }
287 else
288 {
289#ifdef DEBUG
290 std::cout << "TRUE\n";
291#endif
292 return tvt(true);
293 }
294 }
295}
virtual void clear()
Reset the abstract state.
Definition ai.h:265
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
virtual size_t no_variables() const override
Definition cnf.h:42
virtual void write_dimacs_cnf(std::ostream &out) const
mstreamt & error() const
Definition message.h:391
mstreamt & statistics() const
Definition message.h:411
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
tvt l_get(literalt a) const override
std::set< int > assigned
resultt do_prop_solve(const bvt &assumptions) override
std::string pbs_path
virtual void write_dimacs_pb(std::ostream &out)
std::map< literalt, unsigned > pb_constraintmap
resultt
Definition prop.h:101
messaget log
Definition prop.h:134
Definition threeval.h:20
literalt neg(literalt a)
Definition literal.h:193
std::vector< literalt > bvt
Definition literal.h:201
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
int sscanf(const char *restrict s, const char *restrict format,...)
Definition stdio.c:1072
char * getenv(const char *name)
Definition stdlib.c:496