SemOpt  $Revision:83+[c2a47fa11ed3+]$
PreferredSemantics.cpp
Go to the documentation of this file.
1 
9 #include "PreferredSemantics.h"
10 
11 void PreferredSemantics::add_non_emptiness()
12 {
13  OrClause noempty_clause = OrClause();
14  SetArgumentsIterator it_args;
15  for (it_args = af->begin(); it_args != af->end(); it_args++)
16  {
17  noempty_clause.appendVariable((*it_args)->InVar());
18  }
19  this->sat_pigreek.appendOrClause(noempty_clause);
20 }
21 
26  super(the_af, enc)
27 {
28 }
29 
35 {
37  vector<Labelling>::iterator it;
38  bool erased = false;
39  do
40  {
41  erased = false;
42 
43  for (it = this->labellings.begin(); it != this->labellings.end(); it++)
44  {
45  vector<Labelling>::iterator inner;
46  for (inner = this->labellings.begin();
47  inner != this->labellings.end(); inner++)
48  {
49  if (inner == it)
50  continue;
51 
52  if ((*it).inargs()->is_subset((*inner).inargs()))
53  {
54  this->labellings.erase(it);
55  erased = true;
56  break;
57  }
58  }
59  if (erased)
60  break;
61  }
62  } while (erased);
63 }
64 
71 {
72  this->cleanlabs();
73  this->add_non_emptiness();
74  SATFormulae cnf = SATFormulae();
75  this->sat_pigreek.clone(&cnf);
76  do
77  {
78  Labelling prefcand = Labelling();
79  SATFormulae cnfdf = SATFormulae();
80  cnf.clone(&cnfdf);
81 
82  while (true)
83  {
84  Labelling res = Labelling();
85  if(!this->satlab(cnfdf, &res))
86  {
87  break;
88  }
89 
90  if (debug)
91  {
92  cout << endl;
93  cout << "{";
95  for (it = res.inargs()->begin(); it != res.inargs()->end();
96  it++)
97  {
98  cout << (*it)->getName() << " ";
99  }
100  cout << "}" << endl;
101  }
102 
103 
104  res.clone(&prefcand);
105  if (res.inargs()->cardinality() == af->numArgs())
106  break;
107 
109  OrClause remove_complete_from_cnf = OrClause();
110  for (iter = res.inargs()->begin(); iter != res.inargs()->end();
111  iter++)
112  {
113  cnfdf.appendOrClause(OrClause(1, (*iter)->InVar()));
114  remove_complete_from_cnf.appendVariable((*iter)->NotInVar());
115  }
116  cnf.appendOrClause(remove_complete_from_cnf);
117 
118  OrClause remaining = OrClause();
119  for (iter = res.outargs()->begin(); iter != res.outargs()->end();
120  iter++)
121  {
122  remaining.appendVariable((*iter)->InVar());
123  }
124  for (iter = res.undecargs()->begin();
125  iter != res.undecargs()->end(); iter++)
126  {
127  remaining.appendVariable((*iter)->InVar());
128  }
129  cnfdf.appendOrClause(remaining);
130  }
131 
132  if (prefcand.empty())
133  break;
134 
135  this->labellings.push_back(prefcand);
136 
137  OrClause oppsolution = OrClause();
139  for (it = prefcand.outargs()->begin(); it != prefcand.outargs()->end();
140  it++)
141  {
142  oppsolution.appendVariable((*it)->InVar());
143  }
144  for (it = prefcand.undecargs()->begin();
145  it != prefcand.undecargs()->end(); it++)
146  {
147  oppsolution.appendVariable((*it)->InVar());
148  }
149  cnf.appendOrClause(oppsolution);
150 
151  } while (true);
152 
153  if (this->labellings.empty())
154  {
155  this->labellings.push_back(Labelling());
156  }
157 }
158 
159 PreferredSemantics::~PreferredSemantics()
160 {
161  // TODO Auto-generated destructor stub
162 }
163