28 for (it_args =
af->
begin(); it_args !=
af->
end(); it_args++)
34 cout <<
"predecessors of " << (*it_args)->getName() <<
": ";
36 for (it_pred = pred->
begin(); it_pred != pred->
end(); it_pred++)
37 cout << (*it_pred)->getName() <<
" ";
61 OrClause(3, (*it_args)->InVar(), (*it_args)->OutVar(),
62 (*it_args)->UndecVar()));
66 (*it_args)->NotOutVar()));
70 (*it_args)->NotUndecVar()));
74 (*it_args)->NotUndecVar()));
77 for (it_pred = pred->
begin(); it_pred != pred->
end(); it_pred++)
85 (*it_pred)->OutVar()));
100 (*it_args)->OutVar()));
114 OrClause(2, (*it_args)->NotUndecVar(),
115 (*it_pred)->NotInVar()));
154 for (it_pred = pred->
begin(); it_pred != pred->
end(); it_pred++)
157 c3_bigor_clause.
clone(&to_add);
179 stringstream cnf_string(stringstream::in | stringstream::out);
180 sat.
toSS(&cnf_string);
184 cout <<
"Preparing the satsolver" <<
"\n";
185 cout << cnf_string.str();
188 vector<int> lastcompfound = vector<int>();
189 int retsat = (*SatSolver)(&cnf_string, 3 *
af->
numArgs(), sat.
size(),
199 if (lastcompfound.at(i) > 0)
208 if (lastcompfound.at(i +
af->
numArgs()) > 0)
213 if (lastcompfound.at(i + 2 *
af->
numArgs()) > 0)
253 Semantics::~Semantics()
258 Semantics::iterator Semantics::begin()
263 Semantics::iterator Semantics::end()