10 void Preferred::cleanlabs()
12 while (!this->labellings.empty())
13 this->labellings.pop_back();
19 int Preferred::compute_new_pigreek()
22 this->af->get_arguments()->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()));
42 cout <<
"Set arguments: " << endl;
43 cout << *(this->af->get_arguments()) << endl;
45 cout <<
"C set:" << endl;
46 cout << *(this->C) << endl;
51 it_args != this->C->end(); it_args++)
54 if (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
55 || encoding == 4 || encoding == 5)
57 this->sat_new_pigreek.appendOrClause(
58 OrClause(3, (*it_args)->InVar(), (*it_args)->OutVar(),
59 (*it_args)->UndecVar()));
61 this->sat_new_pigreek.appendOrClause(
63 (*it_args)->NotOutVar()));
65 this->sat_new_pigreek.appendOrClause(
67 (*it_args)->NotUndecVar()));
69 this->sat_new_pigreek.appendOrClause(
71 (*it_args)->NotUndecVar()));
80 cout <<
"predecessors of " << (*it_args)->getName() <<
": ";
83 it_pred != pred->
end(); it_pred++)
84 cout << (*it_pred)->getName() <<
" ";
91 this->sat_new_pigreek.appendOrClause(
94 this->sat_new_pigreek.appendOrClause((*it_args)->NotOutVar());
96 this->sat_new_pigreek.appendOrClause((*it_args)->NotUndecVar());
105 it_pred != pred->
end(); it_pred++)
108 if (encoding == 0 || encoding == 1 || encoding == 3
111 this->sat_new_pigreek.appendOrClause(
113 (*it_pred)->OutVar()));
117 if (encoding == 0 || encoding == 2 || encoding == 3
124 if (encoding == 0 || encoding == 1 || encoding == 4
127 this->sat_new_pigreek.appendOrClause(
128 OrClause(2, (*it_args)->NotUndecVar(),
129 (*it_pred)->NotInVar()));
134 if (encoding == 0 || encoding == 2 || encoding == 4
142 if (encoding == 0 || encoding == 2 || encoding == 3
146 this->sat_new_pigreek.appendOrClause(c4_last_clause);
150 if (encoding == 0 || encoding == 1 || encoding == 4
154 this->sat_new_pigreek.appendOrClause(c9_or_undec_clause);
158 if (encoding == 0 || encoding == 2 || encoding == 4
162 it_pred != pred->
end(); it_pred++)
165 c8_bigor_clause.
clone(&to_add);
168 this->sat_new_pigreek.appendOrClause(to_add);
176 it_args != this->af->end(); it_args++)
185 it_pred != pred->
end(); it_pred++)
189 if (encoding == 0 || encoding == 2 || encoding == 3
192 this->sat_new_pigreek.appendOrClause(
194 (*it_args)->OutVar()));
198 if (encoding == 0 || encoding == 1 || encoding == 3
206 if (encoding == 0 || encoding == 1 || encoding == 3 || encoding == 4)
209 this->sat_new_pigreek.appendOrClause(c7_last_clause);
214 this->sat_new_pigreek.appendOrClause(noempty_clause);
216 return this->sat_new_pigreek.size();
228 stringstream cnf_string(stringstream::in | stringstream::out);
229 sat.
toSS(&cnf_string);
233 cout <<
"Preparing the satsolver" <<
"\n";
234 cout << cnf_string.str();
237 vector<int> lastcompfound = vector<int>();
238 int retsat = precosat_lib(&cnf_string, 3 * af->numArgs(), sat.
size(),
246 for (
int i = 0; i < af->numArgs(); i++)
248 if (lastcompfound.at(i) > 0)
253 cout << af->getArgumentByNumber(i)->getName() << endl;
257 if (lastcompfound.at(i + af->numArgs()) > 0)
262 if (lastcompfound.at(i + 2 * af->numArgs()) > 0)
264 lab->
add_label(af->getArgumentByNumber(i),
285 this->compute_new_pigreek();
288 this->sat_new_pigreek.clone(&cnf);
298 if (!this->satlab(cnfdf, &res))
311 cout << (*it)->
getName() <<
" ";
316 res.
clone(&prefcand);
328 this->C->setminus(res.
inargs(), &difference);
330 for (iter = difference.
begin(); iter != difference.
end(); iter++)
337 if (prefcand.
empty())
340 this->labellings.push_back(prefcand);
346 this->C->setminus(prefcand.
inargs(), &difference);
347 for (it = difference.
begin(); it != difference.
end(); it++)
355 if (this->labellings.empty())
361 Preferred::Preferred()
364 this->labellings = vector<Labelling>();
368 Preferred::~Preferred()
373 Preferred::iterator Preferred::begin()
375 return this->labellings.begin();
378 Preferred::iterator Preferred::end()
380 return this->labellings.end();