SemOpt  0.2alpha2-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->af->get_arguments()->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 
40  if (debug)
41  {
42  cout << "Set arguments: " << endl;
43  cout << *(this->af->get_arguments()) << endl;
44 
45  cout << "C set:" << endl;
46  cout << *(this->C) << endl;
47  }
48 
49  OrClause noempty_clause = OrClause();
50  for (SetArgumentsIterator it_args = this->C->begin();
51  it_args != this->C->end(); it_args++)
52  {
53  //c1
54  if (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
55  || encoding == 4 || encoding == 5)
56  {
57  this->sat_new_pigreek.appendOrClause(
58  OrClause(3, (*it_args)->InVar(), (*it_args)->OutVar(),
59  (*it_args)->UndecVar()));
60 
61  this->sat_new_pigreek.appendOrClause(
62  OrClause(2, (*it_args)->NotInVar(),
63  (*it_args)->NotOutVar()));
64 
65  this->sat_new_pigreek.appendOrClause(
66  OrClause(2, (*it_args)->NotInVar(),
67  (*it_args)->NotUndecVar()));
68 
69  this->sat_new_pigreek.appendOrClause(
70  OrClause(2, (*it_args)->NotOutVar(),
71  (*it_args)->NotUndecVar()));
72  }
73 
74  noempty_clause.appendVariable((*it_args)->InVar());
75 
76  SetArguments *pred = (*it_args)->get_attackers();
77 
78  if (debug)
79  {
80  cout << "predecessors of " << (*it_args)->getName() << ": ";
81 
82  for (SetArgumentsIterator it_pred = pred->begin();
83  it_pred != pred->end(); it_pred++)
84  cout << (*it_pred)->getName() << " ";
85  cout << endl;
86  }
87 
88  if (pred->empty())
89  {
90  //c3
91  this->sat_new_pigreek.appendOrClause(
92  OrClause(1, (*it_args)->InVar()));
93 
94  this->sat_new_pigreek.appendOrClause((*it_args)->NotOutVar());
95 
96  this->sat_new_pigreek.appendOrClause((*it_args)->NotUndecVar());
97  }
98  else
99  {
100  OrClause c4_last_clause = OrClause();
101  OrClause c9_or_undec_clause = OrClause();
102  OrClause c8_bigor_clause = OrClause();
103 
104  for (SetArgumentsIterator it_pred = pred->begin();
105  it_pred != pred->end(); it_pred++)
106  {
107  //c5
108  if (encoding == 0 || encoding == 1 || encoding == 3
109  || encoding == 5)
110  {
111  this->sat_new_pigreek.appendOrClause(
112  OrClause(2, (*it_args)->NotInVar(),
113  (*it_pred)->OutVar()));
114  }
115 
116  //c4
117  if (encoding == 0 || encoding == 2 || encoding == 3
118  || encoding == 5)
119  {
120  c4_last_clause.appendVariable((*it_pred)->NotOutVar());
121  }
122 
123  //c9
124  if (encoding == 0 || encoding == 1 || encoding == 4
125  || encoding == 5)
126  {
127  this->sat_new_pigreek.appendOrClause(
128  OrClause(2, (*it_args)->NotUndecVar(),
129  (*it_pred)->NotInVar()));
130 
131  c9_or_undec_clause.appendVariable((*it_pred)->UndecVar());
132  }
133 
134  if (encoding == 0 || encoding == 2 || encoding == 4
135  || encoding == 5)
136  {
137  c8_bigor_clause.appendVariable((*it_pred)->InVar());
138  }
139  }
140 
141  //c4-end
142  if (encoding == 0 || encoding == 2 || encoding == 3
143  || encoding == 5)
144  {
145  c4_last_clause.appendVariable((*it_args)->InVar());
146  this->sat_new_pigreek.appendOrClause(c4_last_clause);
147  }
148 
149  //c9-end
150  if (encoding == 0 || encoding == 1 || encoding == 4
151  || encoding == 5)
152  {
153  c9_or_undec_clause.addHeadVariable((*it_args)->NotUndecVar());
154  this->sat_new_pigreek.appendOrClause(c9_or_undec_clause);
155  }
156 
157  //c8
158  if (encoding == 0 || encoding == 2 || encoding == 4
159  || encoding == 5)
160  {
161  for (SetArgumentsIterator it_pred = pred->begin();
162  it_pred != pred->end(); it_pred++)
163  {
164  OrClause to_add = OrClause();
165  c8_bigor_clause.clone(&to_add);
166  to_add.appendVariable((*it_pred)->NotUndecVar());
167  to_add.appendVariable((*it_args)->UndecVar());
168  this->sat_new_pigreek.appendOrClause(to_add);
169  }
170  }
171 
172  }
173  }
174 
175  for (SetArgumentsIterator it_args = this->af->begin();
176  it_args != this->af->end(); it_args++)
177  {
178  OrClause c7_last_clause = OrClause();
179  SetArguments *pred = (*it_args)->get_attackers();
180 
181  if (pred->empty())
182  continue;
183 
184  for (SetArgumentsIterator it_pred = pred->begin();
185  it_pred != pred->end(); it_pred++)
186  {
187 
188  //c6
189  if (encoding == 0 || encoding == 2 || encoding == 3
190  || encoding == 4)
191  {
192  this->sat_new_pigreek.appendOrClause(
193  OrClause(2, (*it_pred)->NotInVar(),
194  (*it_args)->OutVar()));
195  }
196 
197  //c7
198  if (encoding == 0 || encoding == 1 || encoding == 3
199  || encoding == 4)
200  {
201  c7_last_clause.appendVariable((*it_pred)->InVar());
202  }
203  }
204 
205  //c7-end
206  if (encoding == 0 || encoding == 1 || encoding == 3 || encoding == 4)
207  {
208  c7_last_clause.addHeadVariable((*it_args)->NotOutVar());
209  this->sat_new_pigreek.appendOrClause(c7_last_clause);
210  }
211 
212  }
213 
214  this->sat_new_pigreek.appendOrClause(noempty_clause);
215 
216  return this->sat_new_pigreek.size();
217 }
218 
226 bool Preferred::satlab(SATFormulae sat, Labelling *lab)
227 {
228  stringstream cnf_string(stringstream::in | stringstream::out);
229  sat.toSS(&cnf_string);
230 
231  if (debug)
232  {
233  cout << "Preparing the satsolver" << "\n";
234  cout << cnf_string.str();
235  }
236 
237  vector<int> lastcompfound = vector<int>();
238  int retsat = precosat_lib(&cnf_string, 3 * af->numArgs(), sat.size(),
239  &lastcompfound);
240 
241  if (debug)
242  cout << retsat;
243 
244  if (retsat != 20)
245  {
246  for (int i = 0; i < af->numArgs(); i++)
247  {
248  if (lastcompfound.at(i) > 0)
249  {
250  lab->add_label(af->getArgumentByNumber(i), Labelling::lab_in);
251  if (debug)
252  {
253  cout << af->getArgumentByNumber(i)->getName() << endl;
254  }
255  continue;
256  }
257  if (lastcompfound.at(i + af->numArgs()) > 0)
258  {
259  lab->add_label(af->getArgumentByNumber(i), Labelling::lab_out);
260  continue;
261  }
262  if (lastcompfound.at(i + 2 * af->numArgs()) > 0)
263  {
264  lab->add_label(af->getArgumentByNumber(i),
266  continue;
267  }
268  }
269  if (debug)
270  {
271  cout << "in " << lab->inargs()->cardinality() << endl;
272  cout << "out " << lab->outargs()->cardinality() << endl;
273  cout << "undec " << lab->undecargs()->cardinality() << endl;
274  }
275  return true;
276  }
277  return false;
278 }
279 
280 void Preferred::prefSAT(AF *the_af, SetArguments *the_c)
281 {
282  this->cleanlabs();
283  this->af = the_af;
284  this->C = the_c;
285  this->compute_new_pigreek();
286  SATFormulae cnf = SATFormulae();
287 
288  this->sat_new_pigreek.clone(&cnf);
289  do
290  {
291  Labelling prefcand = Labelling();
292  SATFormulae cnfdf = SATFormulae();
293  cnf.clone(&cnfdf);
294 
295  while (true)
296  {
297  Labelling res = Labelling();
298  if (!this->satlab(cnfdf, &res))
299  {
300  break;
301  }
302 
303  if (debug)
304  {
305  cout << endl;
306  cout << "{";
308  for (it = res.inargs()->begin(); it != res.inargs()->end();
309  it++)
310  {
311  cout << (*it)->getName() << " ";
312  }
313  cout << "}" << endl;
314  }
315 
316  res.clone(&prefcand);
317  if (res.inargs()->cardinality() == C->cardinality())
318  break;
319 
321  for (iter = res.inargs()->begin(); iter != res.inargs()->end();
322  iter++)
323  {
324  cnfdf.appendOrClause(OrClause(1, (*iter)->InVar()));
325  }
326 
327  SetArguments difference = SetArguments();
328  this->C->setminus(res.inargs(), &difference);
329  OrClause remaining = OrClause();
330  for (iter = difference.begin(); iter != difference.end(); iter++)
331  {
332  remaining.appendVariable((*iter)->InVar());
333  }
334  cnfdf.appendOrClause(remaining);
335  }
336 
337  if (prefcand.empty())
338  break;
339 
340  this->labellings.push_back(prefcand);
341 
342  OrClause oppsolution = OrClause();
344 
345  SetArguments difference = SetArguments();
346  this->C->setminus(prefcand.inargs(), &difference);
347  for (it = difference.begin(); it != difference.end(); it++)
348  {
349  oppsolution.appendVariable((*it)->InVar());
350  }
351  cnf.appendOrClause(oppsolution);
352 
353  } while (true);
354 
355  if (this->labellings.empty())
356  {
357  this->labellings.push_back(Labelling());
358  }
359 }
360 
361 Preferred::Preferred()
362 {
363  this->encoding = 0;
364  this->labellings = vector<Labelling>();
365  this->sat_new_pigreek = SATFormulae();
366 }
367 
368 Preferred::~Preferred()
369 {
370 
371 }
372 
373 Preferred::iterator Preferred::begin()
374 {
375  return this->labellings.begin();
376 }
377 
378 Preferred::iterator Preferred::end()
379 {
380  return this->labellings.end();
381 }