SemOpt  0.2alpha5-SCC
Preferred.cpp
1 /*
2  * Preferred.cpp
3  *
4  * Created on: 10 Jun 2013
5  * Author: geryo
6  */
7 
8 #include "Preferred.h"
9 
10 void Preferred::cleanlabs()
11 {
12  while (!this->labellings.empty())
13  this->labellings.pop_back();
14 }
15 
19 int Preferred::compute_new_pigreek()
20 {
21  SetArguments subtraction = SetArguments();
22  this->A->setminus(this->C, &subtraction);
23 
24  for (SetArgumentsIterator it_sub = subtraction.begin();
25  it_sub != subtraction.end(); it_sub++)
26  {
27  if (debug)
28  {
29  cout << "Subtraction " << (*it_sub)->getName() << endl;
30  }
31  //c2
32  this->sat_new_pigreek.appendOrClause(
33  OrClause(1, (*it_sub)->NotInVar()));
34  this->sat_new_pigreek.appendOrClause(
35  OrClause(2, (*it_sub)->OutVar(), (*it_sub)->UndecVar()));
36  this->sat_new_pigreek.appendOrClause(
37  OrClause(2, (*it_sub)->NotOutVar(), (*it_sub)->NotUndecVar()));
38 
39  //c-to-add
40  if ((*it_sub)->get_attackers()->empty())
41  {
42  this->sat_new_pigreek.appendOrClause(OrClause(1, (*it_sub)->UndecVar()));
43  }
44 
45  }
46 
47  if (debug)
48  {
49  cout << "Set arguments: " << endl;
50  cout << *(this->A) << endl;
51 
52  cout << "C set:" << endl;
53  cout << *(this->C) << endl;
54  }
55 
56  OrClause noempty_clause = OrClause();
57  for (SetArgumentsIterator it_args = this->C->begin();
58  it_args != this->C->end(); it_args++)
59  {
60  //c1
61  if (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
62  || encoding == 4 || encoding == 5)
63  {
64  this->sat_new_pigreek.appendOrClause(
65  OrClause(3, (*it_args)->InVar(), (*it_args)->OutVar(),
66  (*it_args)->UndecVar()));
67 
68  this->sat_new_pigreek.appendOrClause(
69  OrClause(2, (*it_args)->NotInVar(),
70  (*it_args)->NotOutVar()));
71 
72  this->sat_new_pigreek.appendOrClause(
73  OrClause(2, (*it_args)->NotInVar(),
74  (*it_args)->NotUndecVar()));
75 
76  this->sat_new_pigreek.appendOrClause(
77  OrClause(2, (*it_args)->NotOutVar(),
78  (*it_args)->NotUndecVar()));
79  }
80 
81  noempty_clause.appendVariable((*it_args)->InVar());
82 
83  SetArguments *pred = (*it_args)->get_attackers();
84 
85  if (debug)
86  {
87  cout << "predecessors of " << (*it_args)->getName() << ": ";
88 
89  for (SetArgumentsIterator it_pred = pred->begin();
90  it_pred != pred->end(); it_pred++)
91  cout << (*it_pred)->getName() << " ";
92  cout << endl;
93  }
94 
95  if (pred->empty())
96  {
97  //c3
98  this->sat_new_pigreek.appendOrClause(
99  OrClause(1, (*it_args)->InVar()));
100 
101  this->sat_new_pigreek.appendOrClause((*it_args)->NotOutVar());
102 
103  this->sat_new_pigreek.appendOrClause((*it_args)->NotUndecVar());
104  }
105  else
106  {
107  OrClause c4_last_clause = OrClause();
108  OrClause c9_or_undec_clause = OrClause();
109  OrClause c8_bigor_clause = OrClause();
110 
111  for (SetArgumentsIterator it_pred = pred->begin();
112  it_pred != pred->end(); it_pred++)
113  {
114 
115  if (!this->A->exists(*it_pred))
116  continue;
117 
118  //c5
119  if (encoding == 0 || encoding == 1 || encoding == 3
120  || encoding == 5)
121  {
122  this->sat_new_pigreek.appendOrClause(
123  OrClause(2, (*it_args)->NotInVar(),
124  (*it_pred)->OutVar()));
125  }
126 
127  //c4
128  if (encoding == 0 || encoding == 2 || encoding == 3
129  || encoding == 5)
130  {
131  c4_last_clause.appendVariable((*it_pred)->NotOutVar());
132  }
133 
134  //c9
135  if (encoding == 0 || encoding == 1 || encoding == 4
136  || encoding == 5)
137  {
138  this->sat_new_pigreek.appendOrClause(
139  OrClause(2, (*it_args)->NotUndecVar(),
140  (*it_pred)->NotInVar()));
141 
142  c9_or_undec_clause.appendVariable((*it_pred)->UndecVar());
143  }
144 
145  if (encoding == 0 || encoding == 2 || encoding == 4
146  || encoding == 5)
147  {
148  c8_bigor_clause.appendVariable((*it_pred)->InVar());
149  }
150  }
151 
152  //c4-end
153  if (encoding == 0 || encoding == 2 || encoding == 3
154  || encoding == 5)
155  {
156  c4_last_clause.appendVariable((*it_args)->InVar());
157  this->sat_new_pigreek.appendOrClause(c4_last_clause);
158  }
159 
160  //c9-end
161  if (encoding == 0 || encoding == 1 || encoding == 4
162  || encoding == 5)
163  {
164  c9_or_undec_clause.addHeadVariable((*it_args)->NotUndecVar());
165  this->sat_new_pigreek.appendOrClause(c9_or_undec_clause);
166  }
167 
168  //c8
169  if (encoding == 0 || encoding == 2 || encoding == 4
170  || encoding == 5)
171  {
172  for (SetArgumentsIterator it_pred = pred->begin();
173  it_pred != pred->end(); it_pred++)
174  {
175  OrClause to_add = OrClause();
176  c8_bigor_clause.clone(&to_add);
177  to_add.appendVariable((*it_pred)->NotUndecVar());
178  to_add.appendVariable((*it_args)->UndecVar());
179  this->sat_new_pigreek.appendOrClause(to_add);
180  }
181  }
182 
183  }
184  }
185 
186  for (SetArgumentsIterator it_args = this->A->begin();
187  it_args != this->A->end(); it_args++)
188  {
189 
190  OrClause c7_last_clause = OrClause();
191  SetArguments *pred = (*it_args)->get_attackers();
192 
193  if (pred->empty())
194  continue;
195 
196  for (SetArgumentsIterator it_pred = pred->begin();
197  it_pred != pred->end(); it_pred++)
198  {
199 
200  if (!this->A->exists(*it_pred))
201  continue;
202 
203  //c6
204  if (encoding == 0 || encoding == 2 || encoding == 3
205  || encoding == 4)
206  {
207  this->sat_new_pigreek.appendOrClause(
208  OrClause(2, (*it_pred)->NotInVar(),
209  (*it_args)->OutVar()));
210  }
211 
212  //c7
213  if (encoding == 0 || encoding == 1 || encoding == 3
214  || encoding == 4)
215  {
216  c7_last_clause.appendVariable((*it_pred)->InVar());
217  }
218  }
219 
220  //c7-end
221  if (encoding == 0 || encoding == 1 || encoding == 3 || encoding == 4)
222  {
223  c7_last_clause.appendVariable((*it_args)->NotOutVar());
224  this->sat_new_pigreek.appendOrClause(c7_last_clause);
225  }
226 
227  }
228 
229  this->sat_new_pigreek.appendOrClause(noempty_clause);
230 
231  return this->sat_new_pigreek.size();
232 }
233 
241 bool Preferred::satlab(SATFormulae sat, Labelling *lab)
242 {
243  stringstream cnf_string(stringstream::in | stringstream::out);
244  sat.toSS(&cnf_string);
245 
246  if (debug)
247  {
248  cout << "Preparing the satsolver" << "\n";
249  cout << cnf_string.str() << endl;
250  }
251 
252  vector<int> lastcompfound = vector<int>();
253  int retsat = precosat_lib(&cnf_string,
254  3 * ((*(this->A->begin()))->get_af()->numArgs()), sat.size(),
255  &lastcompfound);
256 
257  if (debug)
258  {
259  cout << retsat << endl;
260 
261  for (vector<int>::iterator solit = lastcompfound.begin();
262  solit != lastcompfound.end(); solit++)
263  {
264  cout << *solit << " ";
265  }
266  cout << endl;
267  }
268 
269  if (retsat != 20)
270  {
271  for (SetArgumentsIterator it = this->A->begin(); it != this->A->end();
272  it++)
273  {
274  if (find(lastcompfound.begin(), lastcompfound.end(), (*it)->InVar())
275  != lastcompfound.end())
276  {
277  lab->add_label((*it), Labelling::lab_in);
278  if (debug)
279  {
280  cout << (*it)->getName() << endl;
281  }
282  continue;
283  }
284  if (find(lastcompfound.begin(), lastcompfound.end(),
285  (*it)->OutVar()) != lastcompfound.end())
286  {
287  lab->add_label((*it), Labelling::lab_out);
288  continue;
289  }
290  if (find(lastcompfound.begin(), lastcompfound.end(),
291  (*it)->UndecVar()) != lastcompfound.end())
292  {
293  lab->add_label((*it), Labelling::lab_undec);
294  continue;
295  }
296  }
297  if (debug)
298  {
299  cout << endl;
300  cout << "in " << *(lab->inargs()) << endl;
301  cout << "out " << *(lab->outargs()) << endl;
302  cout << "undec " << *(lab->undecargs()) << endl;
303  }
304  return true;
305  }
306  return false;
307 }
308 
309 void Preferred::prefSAT(SetArguments *the_a, SetArguments *the_c)
310 {
311  this->cleanlabs();
312  this->A = the_a;
313  this->C = the_c;
314  this->compute_new_pigreek();
315  SATFormulae cnf = SATFormulae();
316 
317  this->sat_new_pigreek.clone(&cnf);
318  do
319  {
320  Labelling prefcand = Labelling();
321  SATFormulae cnfdf = SATFormulae();
322  cnf.clone(&cnfdf);
323 
324  while (true)
325  {
326  Labelling res = Labelling();
327  if (!this->satlab(cnfdf, &res))
328  {
329  break;
330  }
331 
332  if (debug)
333  {
334  cout << endl;
335  cout << "{";
337  for (it = res.inargs()->begin(); it != res.inargs()->end();
338  it++)
339  {
340  cout << (*it)->getName() << " ";
341  }
342  cout << "}" << endl;
343  }
344 
345  res.clone(&prefcand);
346  if (res.inargs()->cardinality() == C->cardinality())
347  break;
348 
350  for (iter = res.inargs()->begin(); iter != res.inargs()->end();
351  iter++)
352  {
353  cnfdf.appendOrClause(OrClause(1, (*iter)->InVar()));
354  }
355 
356  SetArguments difference = SetArguments();
357  this->C->setminus(res.inargs(), &difference);
358  OrClause remaining = OrClause();
359  for (iter = difference.begin(); iter != difference.end(); iter++)
360  {
361  remaining.appendVariable((*iter)->InVar());
362  }
363  cnfdf.appendOrClause(remaining);
364  }
365 
366  if (prefcand.empty())
367  break;
368 
369  this->labellings.push_back(prefcand);
370 
371  OrClause oppsolution = OrClause();
373 
374  SetArguments difference = SetArguments();
375  this->C->setminus(prefcand.inargs(), &difference);
376  for (it = difference.begin(); it != difference.end(); it++)
377  {
378  oppsolution.appendVariable((*it)->InVar());
379  }
380  cnf.appendOrClause(oppsolution);
381 
382  } while (true);
383 
384  if (this->labellings.empty())
385  {
386  this->labellings.push_back(Labelling());
387  }
388 }
389 
390 Preferred::Preferred()
391 {
392  this->encoding = 0;
393  this->labellings = vector<Labelling>();
394  this->sat_new_pigreek = SATFormulae();
395 }
396 
397 Preferred::~Preferred()
398 {
399 
400 }
401 
402 Preferred::iterator Preferred::begin()
403 {
404  return this->labellings.begin();
405 }
406 
407 Preferred::iterator Preferred::end()
408 {
409  return this->labellings.end();
410 }