SemOpt  $Revision:83+[c2a47fa11ed3+]$
Semantics.cpp
Go to the documentation of this file.
1 
9 #include "Semantics.h"
10 
15 {
16  while (!this->labellings.empty())
17  this->labellings.pop_back();
18 }
19 
25 {
26  SetArgumentsIterator it_args;
27  SetArgumentsIterator it_pred;
28  for (it_args = af->begin(); it_args != af->end(); it_args++)
29  {
30  SetArguments *pred = (*it_args)->get_attackers();
31 
32  if (debug)
33  {
34  cout << "predecessors of " << (*it_args)->getName() << ": ";
35 
36  for (it_pred = pred->begin(); it_pred != pred->end(); it_pred++)
37  cout << (*it_pred)->getName() << " ";
38  cout << endl;
39  }
40 
41  if (pred->empty())
42  {
43  //c2
44  this->sat_pigreek.appendOrClause(OrClause(1, (*it_args)->InVar()));
45 
46  this->sat_pigreek.appendOrClause((*it_args)->NotOutVar());
47 
48  this->sat_pigreek.appendOrClause((*it_args)->NotUndecVar());
49  }
50  else
51  {
52  OrClause c1_last_clause = OrClause();
53  OrClause c2_last_clause = OrClause();
54  OrClause c3_or_undec_clause = OrClause();
55  OrClause c3_bigor_clause = OrClause();
56  //c1
57  if (encoding == 0 || encoding == 1 || encoding == 2 || encoding == 3
58  || encoding == 4 || encoding == 5)
59  {
61  OrClause(3, (*it_args)->InVar(), (*it_args)->OutVar(),
62  (*it_args)->UndecVar()));
63 
65  OrClause(2, (*it_args)->NotInVar(),
66  (*it_args)->NotOutVar()));
67 
69  OrClause(2, (*it_args)->NotInVar(),
70  (*it_args)->NotUndecVar()));
71 
73  OrClause(2, (*it_args)->NotOutVar(),
74  (*it_args)->NotUndecVar()));
75  }
76 
77  for (it_pred = pred->begin(); it_pred != pred->end(); it_pred++)
78  {
79  //c3
80  if (encoding == 0 || encoding == 1 || encoding == 3
81  || encoding == 5)
82  {
84  OrClause(2, (*it_args)->NotInVar(),
85  (*it_pred)->OutVar()));
86  }
87 
88  if (encoding == 0 || encoding == 2 || encoding == 3
89  || encoding == 5)
90  {
91  c1_last_clause.appendVariable((*it_pred)->NotOutVar());
92  }
93 
94  //c4
95  if (encoding == 0 || encoding == 2 || encoding == 3
96  || encoding == 4)
97  {
99  OrClause(2, (*it_pred)->NotInVar(),
100  (*it_args)->OutVar()));
101  }
102 
103  if (encoding == 0 || encoding == 1 || encoding == 3
104  || encoding == 4)
105  {
106  c2_last_clause.appendVariable((*it_pred)->InVar());
107  }
108 
109  //c5
110  if (encoding == 0 || encoding == 1 || encoding == 4
111  || encoding == 5)
112  {
114  OrClause(2, (*it_args)->NotUndecVar(),
115  (*it_pred)->NotInVar()));
116 
117  c3_or_undec_clause.appendVariable((*it_pred)->UndecVar());
118  }
119 
120  if (encoding == 0 || encoding == 2 || encoding == 4
121  || encoding == 5)
122  {
123  c3_bigor_clause.appendVariable((*it_pred)->InVar());
124  }
125  }
126 
127  //c3-end
128  if (encoding == 0 || encoding == 2 || encoding == 3
129  || encoding == 5)
130  {
131  c1_last_clause.appendVariable((*it_args)->InVar());
132  this->sat_pigreek.appendOrClause(c1_last_clause);
133  }
134 
135  //c4-end
136  if (encoding == 0 || encoding == 1 || encoding == 3
137  || encoding == 4)
138  {
139  c2_last_clause.addHeadVariable((*it_args)->NotOutVar());
140  this->sat_pigreek.appendOrClause(c2_last_clause);
141  }
142 
143  //c5-end
144  if (encoding == 0 || encoding == 1 || encoding == 4
145  || encoding == 5)
146  {
147  c3_or_undec_clause.addHeadVariable((*it_args)->NotUndecVar());
148  this->sat_pigreek.appendOrClause(c3_or_undec_clause);
149  }
150 
151  if (encoding == 0 || encoding == 2 || encoding == 4
152  || encoding == 5)
153  {
154  for (it_pred = pred->begin(); it_pred != pred->end(); it_pred++)
155  {
156  OrClause to_add = OrClause();
157  c3_bigor_clause.clone(&to_add);
158  to_add.appendVariable((*it_pred)->NotUndecVar());
159  to_add.appendVariable((*it_args)->UndecVar());
160  this->sat_pigreek.appendOrClause(to_add);
161  }
162  }
163 
164  }
165  }
166 
167  return this->sat_pigreek.size();
168 }
169 
178 {
179  stringstream cnf_string(stringstream::in | stringstream::out);
180  sat.toSS(&cnf_string);
181 
182  if (debug)
183  {
184  cout << "Preparing the satsolver" << "\n";
185  cout << cnf_string.str();
186  }
187 
188  vector<int> lastcompfound = vector<int>();
189  int retsat = (*SatSolver)(&cnf_string, 3 * af->numArgs(), sat.size(),
190  &lastcompfound);
191 
192  if (debug)
193  cout << retsat;
194 
195  if (retsat != 20)
196  {
197  for (int i = 0; i < af->numArgs(); i++)
198  {
199  if (lastcompfound.at(i) > 0)
200  {
202  if (debug)
203  {
204  cout << af->getArgumentByNumber(i)->getName() << endl;
205  }
206  continue;
207  }
208  if (lastcompfound.at(i + af->numArgs()) > 0)
209  {
211  continue;
212  }
213  if (lastcompfound.at(i + 2 * af->numArgs()) > 0)
214  {
216  continue;
217  }
218  }
219  if (debug)
220  {
221  cout << "in " << lab->inargs()->cardinality() << endl;
222  cout << "out " << lab->outargs()->cardinality() << endl;
223  cout << "undec " << lab->undecargs()->cardinality() << endl;
224  }
225  return true;
226  }
227  return false;
228 }
229 
244 Semantics::Semantics(AF *the_af, int enc)
245 {
246  this->af = the_af;
247  this->labellings = vector<Labelling>();
248  this->encoding = enc;
249  this->sat_pigreek = SATFormulae();
251 }
252 
253 Semantics::~Semantics()
254 {
255  // TODO Auto-generated destructor stub
256 }
257 
258 Semantics::iterator Semantics::begin()
259 {
260  return this->labellings.begin();
261 }
262 
263 Semantics::iterator Semantics::end()
264 {
265  return this->labellings.end();
266 }
267