carl  24.04
Computer ARithmetic Library
FormulaPool.tpp
Go to the documentation of this file.
1 /**
2  * @file FormulaPool.tpp
3  *
4  * @author Florian Corzilius<corzilius@cs.rwth-aachen.de>
5  * @author Sebastian Junges
6  * @author Ulrich Loup
7  * @version 2013-10-21
8  */
9 
10 #include "FormulaPool.h"
11 
12 namespace carl
13 {
14  template<typename Pol>
15  FormulaPool<Pol>::FormulaPool( unsigned _capacity ):
16  Singleton<FormulaPool<Pol>>(),
17  mIdAllocator( 3 ),
18  mPoolBuckets(new typename underlying_set::bucket_type[mRehashPolicy.numBucketsFor(_capacity)]),
19  mPool(typename underlying_set::bucket_traits(mPoolBuckets.get(), mRehashPolicy.numBucketsFor(_capacity))),
20  mTseitinVars(),
21  mTseitinVarToFormula()
22  {
23  VariablePool::getInstance();
24  mpTrue = new FormulaContent<Pol>( TRUE, 1 );
25  mpFalse = new FormulaContent<Pol>( FALSE, 2 );
26  mpTrue->mNegation = mpFalse;
27  mpFalse->mNegation = mpTrue;
28  mPool.insert( *mpTrue );
29  mPool.insert( *mpFalse );
30  Formula<Pol>::init( *mpTrue );
31  Formula<Pol>::init( *mpFalse );
32  mpTrue->mUsages = 2; // avoids deleting it
33  mpFalse->mUsages = 2; // avoids deleting it
34  }
35 
36  template<typename Pol>
37  FormulaPool<Pol>::~FormulaPool()
38  {
39  // assert( mPool.size() == 2 );
40  mPool.clear();
41  delete mpTrue;
42  delete mpFalse;
43  }
44 
45  template<typename Pol>
46  const FormulaContent<Pol>* FormulaPool<Pol>::add( FormulaContent<Pol>&& _element )
47  {
48  assert( _element.mType != FormulaType::NOT );
49  FORMULA_POOL_LOCK_GUARD
50 
51  typename underlying_set::insert_commit_data insert_data;
52  auto res = mPool.insert_check(_element, /*content_hash(), content_equal(),*/ insert_data);
53  if( res.second ) // Formula has not yet been generated.
54  {
55  auto cont = new FormulaContent<Pol>(std::move(_element));
56  // Add also the negation of the formula to the pool in order to ensure that it
57  // has the next id and hence would occur next to the formula in a set of sub-formula,
58  // which is sorted by the ids.
59  cont->mId = mIdAllocator;
60  Formula<Pol>::init( *cont );
61  ++mIdAllocator;
62  mPool.insert_commit(*cont, insert_data);
63  check_rehash();
64 
65  auto negation = createNegatedContent(cont);
66  cont->mNegation = negation;
67  negation->mId = mIdAllocator;
68  negation->mNegation = cont;
69  Formula<Pol>::init( *negation );
70  ++mIdAllocator;
71  assert(mPool.find(*negation) == mPool.end());
72  CARL_LOG_DEBUG("carl.formula", "Added " << cont << " / " << negation << " to pool");
73  return cont;
74  } else {
75  CARL_LOG_TRACE("carl.formula", "Found " << static_cast<const void*>(&*res.first) << " in pool");
76  return &*res.first;
77  }
78 
79  }
80 
81  template<typename Pol>
82  bool FormulaPool<Pol>::formulasInverse( const Formula<Pol>& _subformulaA, const Formula<Pol>& _subformulaB )
83  {
84  return _subformulaA.negated() == _subformulaB;
85  }
86 
87  template<typename Pol>
88  const FormulaContent<Pol>* FormulaPool<Pol>::createImplication(Formulas<Pol>&& _subformulas) {
89  assert(_subformulas.size() >= 2);
90  #ifdef SIMPLIFY_FORMULA
91  // Conclusion
92  if (_subformulas.back().mpContent == mpTrue)
93  return create(TRUE);
94  if (_subformulas.back().mpContent == mpFalse) {
95  _subformulas.pop_back();
96  for (auto& f: _subformulas) {
97  f = Formula<Pol>(NOT, f);
98  }
99  return create(OR, std::move(_subformulas));
100  }
101  #endif
102  Formula<Pol> conclusion = _subformulas.back();
103  _subformulas.pop_back();
104  #ifdef SIMPLIFY_FORMULA
105  // Premises
106  for (auto it = _subformulas.begin(); it != _subformulas.end(); ) {
107  if (it->mpContent == mpFalse) return create(TRUE);
108  if (it->mpContent == mpTrue) {
109  auto jt = it;
110  ++jt;
111  if( jt != _subformulas.end() )
112  *it = _subformulas.back();
113  _subformulas.pop_back();
114  }
115  else
116  ++it;
117  }
118  #endif
119  if (_subformulas.empty()) {
120  return conclusion.mpContent;
121  }
122  Formula<Pol> premise(AND, std::move(_subformulas));
123  return add(FormulaContent<Pol>(IMPLIES, {premise, conclusion}));
124  }
125 
126  template<typename Pol>
127  const FormulaContent<Pol>* FormulaPool<Pol>::createNAry(FormulaType _type, Formulas<Pol>&& _subformulas)
128  {
129  assert( _type == FormulaType::AND || _type == FormulaType::OR || _type == FormulaType::XOR || _type == FormulaType::IFF );
130 // std::cout << __func__ << _type;
131 // for( const auto& f : _subformulas )
132 // std::cout << " " << f;
133 // std::cout << std::endl;
134  if( _subformulas.size() == 1 )
135  {
136  CARL_LOG_TRACE("carl.formula", "Only a single subformula, eliminating " << _type);
137  return _subformulas[0].mpContent;
138  }
139  if( _type != FormulaType::IFF )
140  {
141  for( size_t pos = 0; pos < _subformulas.size(); )
142  {
143  if( _subformulas[pos].type() == _type )
144  {
145  // We have (op .. (op a1 .. an) b ..), so create (op .. a1 .. an b ..) instead.
146  // Note, that a1 to an are definitely created before b, as they were sub-formulas
147  // of it, hence, the ids of a1 to an are smaller than the one of b and therefore a1<b .. an<b.
148  // That means, that a1 .. an are inserted into the given set of sub formulas before the position of
149  // b (=iter).
150  // Note also that the operator of a1 to an cannot be oper, as they where also created with this pool.
151  Formula<Pol> tmp = _subformulas[pos];
152  _subformulas[pos] = _subformulas.back();
153  _subformulas.pop_back();
154  _subformulas.insert(_subformulas.end(), tmp.subformulas().begin(), tmp.subformulas().end() );
155  }
156  else
157  ++pos;
158  }
159  }
160  std::sort( _subformulas.begin(), _subformulas.end() );
161  std::vector<Formula<Pol>> subformulas;
162  subformulas.reserve( _subformulas.size() );
163  bool negateResult = false;
164  size_t pos = 0;
165  while( pos < _subformulas.size() && _subformulas[pos].is_true() )
166  {
167  switch( _type )
168  {
169  case FormulaType::XOR:
170  negateResult = !negateResult;
171  break;
172  case FormulaType::OR:
173  return trueFormula();
174  default:
175  assert( _type == FormulaType::AND || _type == FormulaType::IFF );
176  }
177  ++pos;
178  }
179  while( pos < _subformulas.size() && _subformulas[pos].is_false() )
180  {
181  switch( _type )
182  {
183  case FormulaType::IFF:
184  if( _subformulas[0].is_true() )
185  return falseFormula();
186  negateResult = true;
187  break;
188  case FormulaType::AND:
189  return falseFormula();
190  default:
191  assert( _type == FormulaType::OR || _type == FormulaType::XOR );
192  }
193  ++pos;
194  }
195  for( ; pos < _subformulas.size(); )
196  {
197  if( pos < _subformulas.size() - 1 )
198  {
199  if( _subformulas[pos] == _subformulas[pos+1] )
200  {
201  size_t numOfEqualSubformulas = pos;
202  ++pos;
203  while( pos < _subformulas.size() - 1 && _subformulas[pos] == _subformulas[pos+1] )
204  ++pos;
205  if( _type == FormulaType::XOR && (pos + 1 - numOfEqualSubformulas) % 2 == 0 )
206  ++pos;
207  }
208  else if( formulasInverse( _subformulas[pos], _subformulas[pos+1] ) )
209  {
210  // Check if the sub-formula at pos is the negation of the sub-formula at pos+1
211  // Note, that the negation of a formula would by construction always be right after the formula
212  // in a set of formulas whose comparison operator is based on the one of formulas This is due to
213  // them comparing just the ids and we construct the negation of a formula right after the formula
214  // itself and assign the next id to it.
215  switch( _type )
216  {
217  case FormulaType::AND:
218  return falseFormula();
219  case FormulaType::OR:
220  return trueFormula();
221  case FormulaType::IFF:
222  return falseFormula();
223  default:
224  assert( _type == FormulaType::XOR );
225  negateResult = !negateResult;
226  }
227  ++pos;
228  ++pos;
229  }
230  else
231  {
232  subformulas.push_back( _subformulas[pos] );
233  ++pos;
234  }
235  }
236  else
237  {
238  subformulas.push_back( _subformulas[pos] );
239  ++pos;
240  }
241  }
242  if( subformulas.empty() )
243  {
244  if( negateResult || _type == FormulaType::AND || _type == FormulaType::IFF )
245  return trueFormula();
246  return falseFormula();
247  }
248  const FormulaContent<Pol>* result;
249  if( subformulas.size() == 1 )
250  {
251  if( _type == FormulaType::IFF && _subformulas[0] == *subformulas.begin() )
252  return trueFormula();
253  result = subformulas.begin()->mpContent;
254  }
255  else
256  {
257  result = add(FormulaContent<Pol>( _type, std::move( subformulas ) ) );
258  }
259  return negateResult ? result->mNegation : result;
260  }
261 
262  template<typename Pol>
263  const FormulaContent<Pol>* FormulaPool<Pol>::createITE(Formulas<Pol>&& _subformulas) {
264  assert(_subformulas.size() == 3);
265  #ifdef SIMPLIFY_FORMULA
266  Formula<Pol>& condition = _subformulas[0];
267  Formula<Pol>& thencase = _subformulas[1];
268  Formula<Pol>& elsecase = _subformulas[2];
269 
270  if (condition.is_true()) return thencase.mpContent;
271  if (condition.is_false()) return elsecase.mpContent;
272  if (thencase == elsecase) return thencase.mpContent;
273 
274  if (condition.type() == FormulaType::NOT) {
275  _subformulas[0] = condition.subformula();
276  std::swap(_subformulas[1], _subformulas[2]);
277  return createITE(std::move(_subformulas));
278  }
279  if (condition == elsecase) elsecase = Formula<Pol>(falseFormula());
280  if (condition.mpContent == elsecase.mpContent->mNegation) elsecase = Formula<Pol>(trueFormula());
281  if (condition == thencase) thencase = Formula<Pol>(trueFormula());
282  if (condition.mpContent == thencase.mpContent->mNegation) thencase = Formula<Pol>(falseFormula());
283 
284  if (thencase.is_false()) {
285  // (ite c false b) = (~c or false) and (c or b) = ~c and (c or b) = (~c and b)
286  Formulas<Pol> subFormulas;
287  subFormulas.push_back(Formula<Pol>(FormulaType::NOT, condition));
288  subFormulas.push_back(elsecase);
289  return create(FormulaType::AND, std::move(subFormulas));
290  }
291  if (thencase.is_true()) {
292  // (ite c true b) = (~c or true) and (c or b) = (c or b)
293  Formulas<Pol> subFormulas;
294  subFormulas.push_back(condition);
295  subFormulas.push_back(elsecase);
296  return create(FormulaType::OR, std::move(subFormulas));
297  }
298  if (elsecase.is_false()) {
299  // (ite c false b) = (~c or a) and (c or false) = (~c or a) and c = (c and a)
300  Formulas<Pol> subFormulas;
301  subFormulas.push_back(condition);
302  subFormulas.push_back(thencase);
303  return create(FormulaType::AND, std::move(subFormulas));
304  }
305  if (elsecase.is_true()) {
306  // (ite c true b) = (~c or a) and (c or true) = (~c or a)
307  Formulas<Pol> subFormulas;
308  subFormulas.push_back(Formula<Pol>(FormulaType::NOT, condition));
309  subFormulas.push_back(thencase);
310  return create(FormulaType::OR, std::move(subFormulas));
311  }
312  #endif
313  return add(FormulaContent<Pol>(ITE, std::move(_subformulas)));
314  }
315 
316 } // namespace carl