13 string endcl = sep +
"0";
14 string endclnl = endcl + nl;
39 for (
int i = 0; i < (int)af->
numArgs(); i++)
50 for (it = pred->
begin(); it != pred->
end(); it++)
51 cout << (*it)->getName() <<
" ";
58 (*sat).appendOrClause(
72 if (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
73 || encoding == 4 || encoding == 5)
75 (*sat).appendOrClause(
80 (*sat).appendOrClause(
84 (*sat).appendOrClause(
88 (*sat).appendOrClause(
93 for (it = pred->
begin(); it != pred->
end(); it++)
96 if (encoding == 0 || encoding == 1 || encoding == 3
99 (*sat).appendOrClause(
104 if (encoding == 0 || encoding == 2 || encoding == 3
111 if (encoding == 0 || encoding == 2 || encoding == 3
114 (*sat).appendOrClause(
120 if (encoding == 0 || encoding == 1 || encoding == 3
127 if (encoding == 0 || encoding == 1 || encoding == 4
130 (*sat).appendOrClause(
138 if (encoding == 0 || encoding == 2 || encoding == 4
146 if (encoding == 0 || encoding == 2 || encoding == 3 || encoding == 5
150 (*sat).appendOrClause(c1_last_clause);
154 if (encoding == 0 || encoding == 1 || encoding == 3 || encoding == 4
159 (*sat).appendOrClause(c2_last_clause);
163 if (encoding == 0 || encoding == 1 || encoding == 4 || encoding == 5
168 (*sat).appendOrClause(c3_or_undec_clause);
171 if (encoding == 0 || encoding == 2 || encoding == 4 || encoding == 5
174 for (it = pred->
begin(); it != pred->
end(); it++)
177 c3_bigor_clause.
clone(&to_add);
180 (*sat).appendOrClause(to_add);
186 (*sat).appendOrClause(noempty_clause);
188 return (*sat).size();
206 for (
int i = 0; i < (int) (*vals).size(); i++)
230 void INARGS(vector<int> *assign, vector<Argument *> *toarg, vector<Argument *> *closeworld,
AF *af)
232 for (
int i = 0; i < af->
numArgs(); i++)
234 if (assign->at(i) > 0)
288 int PrefSat(
dMatrix *preferred_extensions,
AF *af,
int encoding,
int (*SatSolver)(stringstream *,
int,
int, vector<int> *))
291 vector<vector<int> > intres_temp = vector<vector<int> >();
295 int numcl =
PiGreek(&cnf, af, encoding);
300 ofstream f(
"/tmp/debugcnf");
301 f <<
"p cnf " << 3 * af->
numArgs() <<
" " << numcl <<
"\n"
308 if (SatSolver == NULL)
310 ofstream f(inputfile.append(
".CNF").c_str());
311 f <<
"p cnf " << 3 * af->
numArgs() <<
" " << numcl <<
"\n"
320 vector<int> prefcand = vector<int>();
333 stringstream cnf_string(stringstream::in | stringstream::out);
334 cnfdf.toSS(&cnf_string);
338 cout <<
"Preparing the satsolver" <<
"\n";
339 cout << cnf_string.str();
342 vector<int> lastcompfound = vector<int>();
343 int retsat = (*SatSolver)(&cnf_string, 3 * af->
numArgs(), cnfdf.size(), &lastcompfound);
353 prefcand = vector<int>();
354 for (
int i = 0; i < af->
numArgs(); i++)
355 prefcand.push_back(lastcompfound.at(i));
357 vector<Argument *> in_args = vector<Argument *>();
358 vector<Argument *> in_args_closure = vector<Argument *>();
359 INARGS(&lastcompfound, &in_args, &in_args_closure, af);
364 for (
int i = 0; i < (int)in_args.size(); i++)
366 cout << in_args.at(i)->getName() <<
" ";
371 if ((
int)in_args.size() == af->
numArgs())
375 for (
int i = 0; i < (int)in_args.size(); i++)
377 cnfdf.appendOrClause(
OrClause(1,in_args.at(i)->InVar()));
378 remove_complete_from_cnf.
appendVariable(in_args.at(i)->NotInVar());
380 cnf.appendOrClause(remove_complete_from_cnf);
383 for (
int i = 0; i < (int)in_args_closure.size(); i++)
387 cnfdf.appendOrClause(remaining);
390 if (prefcand.empty())
395 (*preferred_extensions).push_back(vals);
397 vector<Argument *> in_pref = vector<Argument *>();
398 vector<Argument *> in_pref_closure = vector<Argument *>();
399 INARGS(&prefcand, &in_pref, &in_pref_closure, af);
402 for (
int i = 0; i < (int)in_pref_closure.size(); i++)
406 cnf.appendOrClause(oppsolution);
410 if ((*preferred_extensions).empty())
413 for (
int i = 0; i < (int) emptyset.size(); i++)
415 (*preferred_extensions).push_back(emptyset);