10 void Preferred::cleanlabs()
12 while (!this->labellings.empty())
13 this->labellings.pop_back();
19 int Preferred::compute_new_pigreek()
22 this->A->setminus(this->C, &subtraction);
25 it_sub != subtraction.
end(); it_sub++)
29 cout <<
"Subtraction " << (*it_sub)->getName() << endl;
32 this->sat_new_pigreek.appendOrClause(
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()));
40 if ((*it_sub)->get_attackers()->empty())
42 this->sat_new_pigreek.appendOrClause(
OrClause(1, (*it_sub)->UndecVar()));
49 cout <<
"Set arguments: " << endl;
50 cout << *(this->A) << endl;
52 cout <<
"C set:" << endl;
53 cout << *(this->C) << endl;
58 it_args != this->C->end(); it_args++)
61 if (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
62 || encoding == 4 || encoding == 5)
64 this->sat_new_pigreek.appendOrClause(
65 OrClause(3, (*it_args)->InVar(), (*it_args)->OutVar(),
66 (*it_args)->UndecVar()));
68 this->sat_new_pigreek.appendOrClause(
70 (*it_args)->NotOutVar()));
72 this->sat_new_pigreek.appendOrClause(
74 (*it_args)->NotUndecVar()));
76 this->sat_new_pigreek.appendOrClause(
78 (*it_args)->NotUndecVar()));
87 cout <<
"predecessors of " << (*it_args)->getName() <<
": ";
90 it_pred != pred->
end(); it_pred++)
91 cout << (*it_pred)->getName() <<
" ";
98 this->sat_new_pigreek.appendOrClause(
101 this->sat_new_pigreek.appendOrClause((*it_args)->NotOutVar());
103 this->sat_new_pigreek.appendOrClause((*it_args)->NotUndecVar());
112 it_pred != pred->
end(); it_pred++)
115 if (!this->A->exists(*it_pred))
119 if (encoding == 0 || encoding == 1 || encoding == 3
122 this->sat_new_pigreek.appendOrClause(
124 (*it_pred)->OutVar()));
128 if (encoding == 0 || encoding == 2 || encoding == 3
135 if (encoding == 0 || encoding == 1 || encoding == 4
138 this->sat_new_pigreek.appendOrClause(
139 OrClause(2, (*it_args)->NotUndecVar(),
140 (*it_pred)->NotInVar()));
145 if (encoding == 0 || encoding == 2 || encoding == 4
153 if (encoding == 0 || encoding == 2 || encoding == 3
157 this->sat_new_pigreek.appendOrClause(c4_last_clause);
161 if (encoding == 0 || encoding == 1 || encoding == 4
165 this->sat_new_pigreek.appendOrClause(c9_or_undec_clause);
169 if (encoding == 0 || encoding == 2 || encoding == 4
173 it_pred != pred->
end(); it_pred++)
176 c8_bigor_clause.
clone(&to_add);
179 this->sat_new_pigreek.appendOrClause(to_add);
187 it_args != this->A->end(); it_args++)
197 it_pred != pred->
end(); it_pred++)
200 if (!this->A->exists(*it_pred))
204 if (encoding == 0 || encoding == 2 || encoding == 3
207 this->sat_new_pigreek.appendOrClause(
209 (*it_args)->OutVar()));
213 if (encoding == 0 || encoding == 1 || encoding == 3
221 if (encoding == 0 || encoding == 1 || encoding == 3 || encoding == 4)
224 this->sat_new_pigreek.appendOrClause(c7_last_clause);
229 this->sat_new_pigreek.appendOrClause(noempty_clause);
231 return this->sat_new_pigreek.size();
243 stringstream cnf_string(stringstream::in | stringstream::out);
244 sat.
toSS(&cnf_string);
248 cout <<
"Preparing the satsolver" <<
"\n";
249 cout << cnf_string.str() << endl;
252 vector<int> lastcompfound = vector<int>();
253 int retsat = precosat_lib(&cnf_string,
254 3 * ((*(this->A->begin()))->get_af()->numArgs()), sat.
size(),
259 cout << retsat << endl;
261 for (vector<int>::iterator solit = lastcompfound.begin();
262 solit != lastcompfound.end(); solit++)
264 cout << *solit <<
" ";
274 if (find(lastcompfound.begin(), lastcompfound.end(), (*it)->InVar())
275 != lastcompfound.end())
280 cout << (*it)->getName() << endl;
284 if (find(lastcompfound.begin(), lastcompfound.end(),
285 (*it)->OutVar()) != lastcompfound.end())
290 if (find(lastcompfound.begin(), lastcompfound.end(),
291 (*it)->UndecVar()) != lastcompfound.end())
300 cout <<
"in " << *(lab->
inargs()) << endl;
301 cout <<
"out " << *(lab->
outargs()) << endl;
302 cout <<
"undec " << *(lab->
undecargs()) << endl;
314 this->compute_new_pigreek();
317 this->sat_new_pigreek.clone(&cnf);
327 if (!this->satlab(cnfdf, &res))
340 cout << (*it)->
getName() <<
" ";
345 res.
clone(&prefcand);
357 this->C->setminus(res.
inargs(), &difference);
359 for (iter = difference.
begin(); iter != difference.
end(); iter++)
366 if (prefcand.
empty())
369 this->labellings.push_back(prefcand);
375 this->C->setminus(prefcand.
inargs(), &difference);
376 for (it = difference.
begin(); it != difference.
end(); it++)
384 if (this->labellings.empty())
390 Preferred::Preferred()
393 this->labellings = vector<Labelling>();
397 Preferred::~Preferred()
402 Preferred::iterator Preferred::begin()
404 return this->labellings.begin();
407 Preferred::iterator Preferred::end()
409 return this->labellings.end();