COPASI API  4.16.103
CNormalLogical.cpp
Go to the documentation of this file.
1 // Copyright (C) 2010 - 2013 by Pedro Mendes, Virginia Tech Intellectual
2 // Properties, Inc., University of Heidelberg, and The University
3 // of Manchester.
4 // All rights reserved.
5 
6 // Copyright (C) 2008 - 2009 by Pedro Mendes, Virginia Tech Intellectual
7 // Properties, Inc., EML Research, gGmbH, University of Heidelberg,
8 // and The University of Manchester.
9 // All rights reserved.
10 
11 // Copyright (C) 2007 by Pedro Mendes, Virginia Tech Intellectual
12 // Properties, Inc. and EML Research, gGmbH.
13 // All rights reserved.
14 
15 #ifdef WIN32
16 # pragma warning (disable: 4786)
17 # pragma warning (disable: 4243)
18 // warning C4355: 'this' : used in base member initializer list
19 # pragma warning (disable: 4355)
20 #endif // WIN32
21 
22 #include <vector>
23 #include <bitset>
24 #include <sstream>
25 #include <algorithm>
26 
27 #include <assert.h>
28 
29 #include "CNormalLogical.h"
30 #include "CNormalChoiceLogical.h"
31 #include "CNormalLogicalItem.h"
32 
34 {}
35 
37 {
38  cleanSetOfSets(this->mChoices);
39  copySetOfSets(src.mChoices, this->mChoices);
40  cleanSetOfSets(this->mAndSets);
41  copySetOfSets(src.mAndSets, this->mAndSets);
42 }
43 
45 {
46  this->mNot = src.mNot;
47  cleanSetOfSets(this->mChoices);
48  copySetOfSets(src.mChoices, this->mChoices);
49  cleanSetOfSets(this->mAndSets);
50  copySetOfSets(src.mAndSets, this->mAndSets);
51  return *this;
52 }
53 
55 {
56  cleanSetOfSets(this->mChoices);
57  cleanSetOfSets(this->mAndSets);
58 }
59 
61 {
62  return new CNormalLogical(*this);
63 }
64 
65 std::string CNormalLogical::toString() const
66 {
67  std::ostringstream str;
68 
69  if (this->mNot == true)
70  {
71  str << "NOT ";
72  }
73 
74  str << "(";
75  ChoiceSetOfSets::const_iterator it = this->mChoices.begin(), endit = this->mChoices.end();
76 
77  while (it != endit)
78  {
79  if (it->second == true)
80  {
81  str << "NOT ";
82  }
83 
84  str << "(";
85  ChoiceSet::const_iterator inner = it->first.begin(), innerend = it->first.end();
86 
87  while (inner != innerend)
88  {
89  if (inner->second == true)
90  {
91  str << "NOT (" << inner->first->toString() << ")";
92  }
93  else
94  {
95  str << inner->first->toString();
96  }
97 
98  ++inner;
99 
100  if (inner != innerend)
101  {
102  str << " & ";
103  }
104  }
105 
106  str << ")";
107  ++it;
108 
109  if (it != endit)
110  {
111  str << " | ";
112  }
113  }
114 
115  ItemSetOfSets::const_iterator it2 = this->mAndSets.begin(), endit2 = this->mAndSets.end();
116 
117  while (it2 != endit2)
118  {
119  if (it2->second == true)
120  {
121  str << "NOT ";
122  }
123 
124  str << "(";
125  ItemSet::const_iterator inner = it2->first.begin(), innerend = it2->first.end();
126 
127  while (inner != innerend)
128  {
129  if (inner->second == true)
130  {
131  str << "NOT (" << inner->first->toString() << ")";
132  }
133  else
134  {
135  str << inner->first->toString();
136  }
137 
138  ++inner;
139 
140  if (inner != innerend)
141  {
142  str << " & ";
143  }
144  }
145 
146  str << ")";
147  ++it2;
148 
149  if (it2 != endit2)
150  {
151  str << " | ";
152  }
153  }
154 
155  str << ")";
156  return str.str();
157 }
158 
160 {
161  return this->mNot;
162 }
163 
165 {
166  this->mNot = negate;
167 }
168 
170 {
171  this->mNot = !this->mNot;
172 }
173 
174 std::ostream& operator<<(std::ostream& os, const CNormalLogical& logical)
175 {
176  os << logical.toString();
177  return os;
178 }
179 
181 {
182  return this->mChoices;
183 }
184 
186 {
187  return this->mChoices;
188 }
189 
191 {
192  return this->mAndSets;
193 }
194 
196 {
197  return this->mAndSets;
198 }
199 
201 {
202  bool result = true;
203  // get rid of the choices
204  ChoiceSetOfSets::const_iterator it = this->mChoices.begin(), endit = this->mChoices.end();
205 
206  while (it != endit && result == true)
207  {
208  ChoiceSet tmpSet;
209 
210  if ((*it).second == true)
211  {
212  result = negateSets((*it).first, tmpSet);
213  }
214  else
215  {
216  copySet((*it).first, tmpSet);
217  }
218 
219  ChoiceSet::iterator it2 = tmpSet.begin(), endit2 = tmpSet.end();
220 
221  while (it2 != endit2 && result == true)
222  {
223  if ((*it2).second == true)
224  {
225  (*it2).first->negate();
226  }
227 
228  (*it2).first->simplify();
229 
230  ItemSetOfSets* set1[4];
231  ItemSetOfSets* set2[2];
232 
233  const CNormalLogical* pLogical = &it2->first->getCondition();
234  assert(pLogical != NULL);
235  assert(pLogical->getChoices().size() == 0);
236  ItemSetOfSets* itemSetOfSets = new ItemSetOfSets();
237 
238  if (pLogical->isNegated())
239  {
240  ItemSetOfSets tmpSetOfSets;
241  negateSetOfSets(pLogical->getAndSets(), *itemSetOfSets);
242  convertAndOrToOrAnd(*itemSetOfSets, tmpSetOfSets);
243  cleanSetOfSets(*itemSetOfSets);
244  eliminateNullItems(tmpSetOfSets, *itemSetOfSets, true);
245  cleanSetOfSets(tmpSetOfSets);
246  }
247  else
248  {
249  copySetOfSets(pLogical->getAndSets(), *itemSetOfSets);
250  }
251 
252  set1[0] = itemSetOfSets;
253  pLogical = &it2->first->getTrueExpression();
254  assert(pLogical != NULL);
255  assert(pLogical->getChoices().size() == 0);
256  itemSetOfSets = new ItemSetOfSets();
257 
258  if (pLogical->isNegated())
259  {
260  ItemSetOfSets tmpSetOfSets;
261  negateSetOfSets(pLogical->getAndSets(), *itemSetOfSets);
262  convertAndOrToOrAnd(*itemSetOfSets, tmpSetOfSets);
263  cleanSetOfSets(*itemSetOfSets);
264  eliminateNullItems(tmpSetOfSets, *itemSetOfSets, true);
265  cleanSetOfSets(tmpSetOfSets);
266  }
267  else
268  {
269  copySetOfSets(pLogical->getAndSets(), *itemSetOfSets);
270  }
271 
272  set1[1] = itemSetOfSets;
273  pLogical = dynamic_cast<const CNormalLogical*>(it2->first->getCondition().copy());
274  const_cast<CNormalLogical*>(pLogical)->negate();
275  assert(pLogical != NULL);
276  assert(pLogical->getChoices().size() == 0);
277  itemSetOfSets = new ItemSetOfSets();
278 
279  if (pLogical->isNegated())
280  {
281  ItemSetOfSets tmpSetOfSets;
282  negateSetOfSets(pLogical->getAndSets(), *itemSetOfSets);
283  convertAndOrToOrAnd(*itemSetOfSets, tmpSetOfSets);
284  cleanSetOfSets(*itemSetOfSets);
285  eliminateNullItems(tmpSetOfSets, *itemSetOfSets, true);
286  cleanSetOfSets(tmpSetOfSets);
287  }
288  else
289  {
290  copySetOfSets(pLogical->getAndSets(), *itemSetOfSets);
291  }
292 
293  set1[2] = itemSetOfSets;
294  delete pLogical;
295  pLogical = &it2->first->getFalseExpression();
296  assert(pLogical != NULL);
297  assert(pLogical->getChoices().size() == 0);
298  itemSetOfSets = new ItemSetOfSets();
299 
300  if (pLogical->isNegated())
301  {
302  ItemSetOfSets tmpSetOfSets;
303  negateSetOfSets(pLogical->getAndSets(), *itemSetOfSets);
304  convertAndOrToOrAnd(*itemSetOfSets, tmpSetOfSets);
305  cleanSetOfSets(*itemSetOfSets);
306  eliminateNullItems(tmpSetOfSets, *itemSetOfSets, true);
307  cleanSetOfSets(tmpSetOfSets);
308  }
309  else
310  {
311  copySetOfSets(pLogical->getAndSets(), *itemSetOfSets);
312  }
313 
314  set1[3] = itemSetOfSets;
315 
316  ItemSetOfSets tmpSetOfSets;
317  itemSetOfSets = new ItemSetOfSets();
318  convertAndOrToOrAnd(*set1[0], tmpSetOfSets);
319  convertAndOrToOrAnd(*set1[1], tmpSetOfSets);
320  eliminateNullItems(tmpSetOfSets, *itemSetOfSets, false);
321  cleanSetOfSets(tmpSetOfSets);
322  set2[0] = itemSetOfSets;
323 
324  itemSetOfSets = new ItemSetOfSets();
325  convertAndOrToOrAnd(*set1[2], tmpSetOfSets);
326  convertAndOrToOrAnd(*set1[3], tmpSetOfSets);
327  eliminateNullItems(tmpSetOfSets, *itemSetOfSets, false);
328  cleanSetOfSets(tmpSetOfSets);
329  set2[1] = itemSetOfSets;
330  cleanSetOfSets(*set1[0]);
331  delete set1[0];
332  cleanSetOfSets(*set1[1]);
333  delete set1[1];
334  cleanSetOfSets(*set1[2]);
335  delete set1[2];
336  cleanSetOfSets(*set1[3]);
337  delete set1[3];
338  itemSetOfSets = new ItemSetOfSets();
339  convertAndOrToOrAnd(*set2[0], tmpSetOfSets);
340  convertAndOrToOrAnd(*set2[1], tmpSetOfSets);
341  eliminateNullItems(tmpSetOfSets, *itemSetOfSets, true);
342  cleanSetOfSets(tmpSetOfSets);
343 
344  /**
345  * Out of some reason, I can not use the insert method becasuse this
346  * seems to lead to different results in certain cases. E.g. I had a
347  * itemSetOfSets with 17 entries and if I used the insert, only 15
348  * eneded up in mAndItems, whereas when I copied them in a loop, all
349  * 17 ended up in mAndItems.
350  * This is strange and unsatisfying, but since sets can't be debuged
351  * that well, I didn't feel like digging into this.
352  * RG
353  */
354  //this->mAndSets.insert(itemSetOfSets->begin(), itemSetOfSets->end());
355  ItemSetOfSets::const_iterator tmpIt = itemSetOfSets->begin(), tmpEndit = itemSetOfSets->end();
356 
357  while (tmpIt != tmpEndit)
358  {
359  /*std::pair<ItemSetOfSets::iterator, bool> tmpResult = */
360  this->mAndSets.insert(*tmpIt);
361  ++tmpIt;
362  }
363 
364  cleanSetOfSets(*set2[0]);
365  delete set2[0];
366  cleanSetOfSets(*set2[1]);
367  delete set2[1];
368  delete itemSetOfSets;
369  ++it2;
370  }
371 
372  cleanSet(tmpSet);
373  tmpSet.clear();
374  ++it;
375  }
376 
377  if (result == true)
378  {
379  // we can assume that all choices have been converted, so we clean the
380  // data structure
381  cleanSetOfSets(this->mChoices);
382 
383  // get rid of the mNot if it is set
384  if (this->mNot == true)
385  {
386  ItemSetOfSets tmpSetOfSets;
387  result = negateSetOfSets(this->mAndSets, tmpSetOfSets);
388 
389  if (result == true)
390  {
391  cleanSetOfSets(this->mAndSets);
392  convertAndOrToOrAnd(tmpSetOfSets, this->mAndSets);
393  cleanSetOfSets(tmpSetOfSets);
394  this->mNot = false;
395  }
396  else
397  {
398  cleanSetOfSets(tmpSetOfSets);
399  }
400  }
401 
402  ItemSetOfSets::iterator it2 = this->mAndSets.begin(), endit2 = this->mAndSets.end();
403  ItemSetOfSets tmpAndSets;
404  eliminateNullItems(this->mAndSets, tmpAndSets, true);
405  cleanSetOfSets(tmpAndSets);
406 
407  while (it2 != endit2)
408  {
409  // get rid of all not flags within the items.
410  // and simplify all items
411  assert((*it2).second == false);
412  ItemSet::iterator it3 = (*it2).first.begin(), endit3 = (*it2).first.end();
413 
414  while (it3 != endit3)
415  {
416  assert((*it3).second == false);
417  (*it3).first->simplify();
418  ++it3;
419  }
420 
421  // check if one item is equal to negating another item
422  // if this is the case, the whole set can be replaced by false
423  // because B AND NOT(B) is always false
424  // also if we find a FALSE item, we can eliminate all others
425  bool eliminate = false;
426  it3 = (*it2).first.begin();
427 
428  if (it3 != endit3)
429  {
430  --endit3;
431  }
432 
433  CNormalLogicalItem* pItem1;
434  CNormalLogicalItem* pItem2;
435 
436  while (it3 != endit3 && eliminate == false)
437  {
438  pItem1 = new CNormalLogicalItem(*(*it3).first);
439 
440  if (pItem1->getType() == CNormalLogicalItem::FALSE)
441  {
442  eliminate = true;
443  delete pItem1;
444  break;
445  }
446 
447  pItem1->negate();
448  ItemSet::iterator it4 = it3, endit4 = (*it2).first.end();
449 
450  if (it4 != endit4)
451  {
452  ++it4;
453  }
454 
455  while (it4 != endit4 && eliminate == false)
456  {
457  pItem2 = (*it4).first;
458 
459  if (pItem2->getType() == CNormalLogicalItem::FALSE)
460  {
461  eliminate = true;
462  break;
463  }
464 
465  if ((*pItem2) == (*pItem1))
466  {
467  eliminate = true;
468  break;
469  }
470 
471  ++it4;
472  }
473 
474  delete pItem1;
475  ++it3;
476  }
477 
478  if (eliminate == true)
479  {
480  ItemSet tmpSet;
481  CNormalLogicalItem* pLogical = new CNormalLogicalItem();
483  tmpSet.insert(std::make_pair(pLogical, false));
484 
485  if (tmpAndSets.insert(std::make_pair(tmpSet, false)).second == false)
486  {
487  cleanSet(tmpSet);
488  tmpSet.clear();
489  }
490  }
491  else
492  {
493  ItemSet tmpSet;
494  copySet((*it2).first, tmpSet);
495 
496  if (tmpAndSets.insert(std::make_pair(tmpSet, false)).second == false)
497  {
498  cleanSet(tmpSet);
499  tmpSet.clear();
500  }
501  }
502 
503  ++it2;
504  }
505 
506  cleanSetOfSets(this->mAndSets);
507  this->mAndSets = tmpAndSets;
508  // simplify the sets, e.g. if one item in an AND combination is false, the
509  // whole set can be replaced by one FALSE item
510  // likewise if one item in an OR set is TRUE, the whole set can be replaced
511  // by one TRUE item
512  //
513  it2 = this->mAndSets.begin(), endit2 = this->mAndSets.end();
514 
515  if (it2 != endit2)
516  {
517  --endit2;
518  }
519 
520  bool eliminate = false;
521  CNormalLogicalItem* pLogicalItem1, *pLogicalItem2;
522 
523  while (it2 != endit2 && eliminate == false)
524  {
525  // if the set in it2 contains only one item and that item is a true
526  // item, we can eliminate all other sets
527  if ((*it2).first.size() == 1)
528  {
529  pLogicalItem1 = new CNormalLogicalItem(*(*(*it2).first.begin()).first);
530 
531  if (pLogicalItem1->getType() == CNormalLogicalItem::TRUE)
532  {
533  eliminate = true;
534  delete pLogicalItem1;
535  break;
536  }
537 
538  pLogicalItem1->negate();
539  ItemSetOfSets::iterator it3 = it2, endit3 = this->mAndSets.end();
540  ++it3;
541 
542  while (it3 != endit3 && eliminate == false)
543  {
544  if ((*it3).first.size() == 1)
545  {
546  pLogicalItem2 = (*(*it3).first.begin()).first;
547 
548  if ((*pLogicalItem1) == (*pLogicalItem2))
549  {
550  eliminate = true;
551  delete pLogicalItem1;
552  break;
553  }
554  }
555 
556  ++it3;
557  }
558 
559  delete pLogicalItem1;
560  }
561 
562  ++it2;
563  }
564 
565  if (eliminate == true)
566  {
567  cleanSetOfSets(this->mAndSets);
568  ItemSet tmpSet;
569  CNormalLogicalItem* pLogical = new CNormalLogicalItem();
571  tmpSet.insert(std::make_pair(pLogical, false));
572  this->mAndSets.insert(std::make_pair(tmpSet, false));
573  }
574  }
575 
576  // now we go through all or combined sets if there are more then one and
577  // erase all FALSE items
578  if (this->mAndSets.size() > 1)
579  {
580  // there can be only one set that contains only one false item
581  // in mAndSets since it is a set and the sorter eliminates all
582  // others
583  ItemSet tmpSet;
584  CNormalLogicalItem* pFalseItem = new CNormalLogicalItem();
585  pFalseItem->setType(CNormalLogicalItem::FALSE);
586  tmpSet.insert(std::make_pair(pFalseItem, false));
587  std::pair<ItemSet, bool> falsePair = std::make_pair(tmpSet, false);
588  this->mAndSets.erase(falsePair);
589  delete pFalseItem;
590  }
591 
592  // since we worked on the objects in the sets, we might have messed up the order of
593  // objects, or some objects might be in there twice, so to fix this, we copy the set
594  ItemSetOfSets::iterator it2 = this->mAndSets.begin();
595  ItemSetOfSets::iterator endit2 = this->mAndSets.end();
596  ItemSetOfSets tmpSet;
597  CNormalLogicalItem* pTrueItem = new CNormalLogicalItem();
598  pTrueItem->setType(CNormalLogicalItem::TRUE);
599  std::pair<CNormalLogicalItem*, bool> truePair = std::make_pair(pTrueItem, false);
600 
601  while (it2 != endit2)
602  {
603  ItemSet tmpSet2(it2->first);
604 
605  // while we are at it, we also delete all TRUE items in the inner sets
606  // if those have more than one item
607  // there can be only one true item per set since it
608  // is a set and the sorter eliminates all others
609  if (tmpSet2.size() > 1)
610  {
611  tmpSet2.erase(truePair);
612  }
613 
614  if (tmpSet.insert(std::make_pair(tmpSet2, it2->second)).second == false)
615  {
616  // delete the items in this set.
617  cleanSet(tmpSet2);
618  tmpSet.clear();
619  }
620 
621  ++it2;
622  }
623 
624  delete pTrueItem;
625  this->mAndSets.clear();
626  this->mAndSets = tmpSet;
627  tmpSet.clear();
628  eliminateNullItems(this->mAndSets, tmpSet, true);
629  cleanSetOfSets(tmpSet);
630 
631  if ((result = this->generateCanonicalDNF(tmpSet)))
632  {
633  cleanSetOfSets(this->mAndSets);
634  this->mAndSets = tmpSet;
635  }
636  else
637  {
638  cleanSetOfSets(tmpSet);
639  }
640 
641  return result;
642 }
643 
644 /**
645  * Converts a set of AND combined sets of OR combined elements into a
646  * target set of OR combined sets of AND combined elements.
647  */
648 
649 /**
650  * Negates a set of elements.
651  * The result of the operation is returned in target.
652  * The type of result depends on the source. If the source was a set of AND
653  * combined elements, the result is a set of OR combined elements and vice versa.
654  * target set.
655  */
656 /**
657  * Negates a set of sets with elements.
658  * The result of the operation is returned in target.
659  * The type of the result depends on the source.
660  * If the source was a set of AND combined sets of OR combined
661  * elements, the rersult will be a set of OR combined sets with AND combined
662  * elements.
663  */
664 
666 {
667  bool result = true;
668 
669  if (this->mNot == rhs.mNot)
670  {
671  if (this->mChoices.size() != rhs.mChoices.size() || this->mAndSets.size() != rhs.mAndSets.size())
672  {
673  result = false;
674  }
675  else
676  {
677  ChoiceSetOfSets::const_iterator it = this->mChoices.begin(), endit = this->mChoices.end(), it2 = rhs.mChoices.begin();
679 
680  while (it != endit)
681  {
682  if (comp.isEqual((*it), (*it2)) == false)
683  {
684  result = false;
685  break;
686  }
687 
688  ++it;
689  ++it2;
690  }
691 
692  ItemSetOfSets::const_iterator it3 = this->mAndSets.begin(), endit3 = this->mAndSets.end(), it4 = rhs.mAndSets.begin();
694 
695  while (it3 != endit3 && result == true)
696  {
697  if (comp2.isEqual((*it3), (*it4)) == false)
698  {
699  result = false;
700  break;
701  }
702 
703  ++it3;
704  ++it4;
705  }
706  }
707  }
708  else
709  {
710  result = false;
711  }
712 
713  return result;
714 }
715 
717 {
718  bool result = true;
719 
720  if (this->mNot == false && rhs.mNot == true)
721  {
722  result = false;
723  }
724  else if (this->mNot == rhs.mNot)
725  {
726  if (this->mChoices.size() < rhs.mChoices.size())
727  {
728  result = false;
729  }
730  else if (this->mChoices.size() == rhs.mChoices.size())
731  {
732  ChoiceSetOfSets::const_iterator it = this->mChoices.begin(), endit = this->mChoices.end(), it2 = rhs.mChoices.begin();
734 
735  while (it != endit)
736  {
737  if (comp((*it), (*it2)) == false)
738  {
739  result = false;
740  break;
741  }
742 
743  ++it;
744  ++it2;
745  }
746 
747  if (result == true)
748  {
749  if (this->mAndSets.size() > rhs.mAndSets.size())
750  {
751  result = false;
752  }
753  else if (this->mAndSets.size() == rhs.mAndSets.size())
754  {
755  ItemSetOfSets::const_iterator it3 = this->mAndSets.begin(), endit3 = this->mAndSets.end(), it4 = rhs.mAndSets.begin();
757 
758  while (it3 != endit3)
759  {
760  if (comp2((*it3), (*it4)) == false)
761  {
762  result = false;
763  break;
764  }
765 
766  ++it3;
767  ++it4;
768  }
769  }
770  }
771  }
772  }
773 
774  return result;
775 }
776 
778 {
779  cleanSetOfSets(this->mAndSets);
780  this->mAndSets.clear();
781  copySetOfSets(set, this->mAndSets);
782 }
783 
785 {
786  cleanSetOfSets(this->mChoices);
787  this->mChoices.clear();
788  copySetOfSets(set, this->mChoices);
789 }
790 
791 /*
792 std::string CNormalLogical::debug() const
793 {
794  std::ostringstream os;
795  os << "Logical: " << *this << std::endl;
796  CNormalLogical::ItemSetOfSets::const_iterator it=this->mAndSets.begin();
797  CNormalLogical::ItemSetOfSets::const_iterator endit=this->mAndSets.end();
798  while(it!=endit)
799  {
800  os << "new set with " << it->first.size() << " items." << std::endl;
801  CNormalLogical::ItemSet::const_iterator it2=it->first.begin();
802  CNormalLogical::ItemSet::const_iterator endit2=it->first.end();
803  while(it2!=endit2)
804  {
805  os << "item: " << *(it2->first) << std::endl;
806  os << "item left: " << it2->first->getLeft() << std::endl;
807  os << "item right: " << it2->first->getRight() << std::endl;
808  ++it2;
809  }
810  ++it;
811  }
812  return os.str();
813 }
814 
815 std::set<const CNormalLogical*> CNormalLogical::findLogicals() const
816 {
817  std::set<const CNormalLogical*> set;
818  ChoiceSetOfSets::const_iterator it=this->mChoices.begin();
819  ChoiceSetOfSets::const_iterator endit=this->mChoices.end();
820  while(it!=endit)
821  {
822  ChoiceSet::const_iterator it2=it->first.begin();
823  ChoiceSet::const_iterator endit2=it->first.end();
824  while(it2!=endit2)
825  {
826  set.insert(&(*it2).first->getCondition());
827  std::set<const CNormalLogical*> tmpSet=(*it2).first->getCondition().findLogicals();
828  set.insert(tmpSet.begin(),tmpSet.end());
829  set.insert(&(*it2).first->getTrueExpression());
830  tmpSet.clear();
831  tmpSet=(*it2).first->getTrueExpression().findLogicals();
832  set.insert(tmpSet.begin(),tmpSet.end());
833  set.insert(&(*it2).first->getFalseExpression());
834  tmpSet.clear();
835  tmpSet=(*it2).first->getFalseExpression().findLogicals();
836  set.insert(tmpSet.begin(),tmpSet.end());
837  ++it2;
838  }
839  ++it;
840  }
841  return set;
842 }
843  */
844 
846 {
847  bool result = true;
848 
849  if (this->mChoices.empty() && !this->mAndSets.empty())
850  {
851  // first we have to create a map with logical items as the keys
852  // the sorting should be OK since CNormalLogicalItem implements the
853  // less operator.
854  std::map<CNormalLogicalItem, bool> truthValueMap;
855  ItemSetOfSets::const_iterator outerIt = this->mAndSets.begin(), outerEndit = this->mAndSets.end();
856 
857  while (outerIt != outerEndit && result == true)
858  {
859  result = (outerIt->second == false);
860  ItemSet::const_iterator innerIt = outerIt->first.begin(), innerEndit = outerIt->first.end();
861 
862  while (innerIt != innerEndit && result == true)
863  {
864  result = (innerIt->second == false);
865  truthValueMap[*(innerIt->first)] = false;
866  ++innerIt;
867  }
868 
869  ++outerIt;
870  }
871 
872  if (truthValueMap.size() <= 16)
873  {
874  std::vector<CNormalLogicalItem> itemVector;
875  std::map<CNormalLogicalItem, bool>::const_iterator mapIt = truthValueMap.begin(), mapEndit = truthValueMap.end();
876 
877  while (mapIt != mapEndit)
878  {
879  // only add the item if the negated item is not already part
880  // of the vector
881  CNormalLogicalItem* pNegatedItem = new CNormalLogicalItem(mapIt->first);
882  pNegatedItem->negate();
883  pNegatedItem->simplify();
884 
885  if (std::find(itemVector.begin(), itemVector.end(), *pNegatedItem) == itemVector.end())
886  {
887  itemVector.push_back(mapIt->first);
888  }
889 
890  delete pNegatedItem;
891  ++mapIt;
892  }
893 
894  unsigned int i = 0, iMax = (1 << itemVector.size());
895 
896  while (i < iMax && result == true)
897  {
898  // create a new row for the truth table
899  // the bits in i can be mapped to the truth values
900  std::bitset<16> bitSet((unsigned long long)i);
901  unsigned int j, jMax = itemVector.size();
902 
903  for (j = 0; j < jMax; ++j)
904  {
905  truthValueMap[itemVector[j]] = bitSet[j];
906  // set the truth value for the negated item if it is in the
907  // map
908  CNormalLogicalItem* pNegatedItem = new CNormalLogicalItem(itemVector[j]);
909  pNegatedItem->negate();
910  pNegatedItem->simplify();
911 
912  if (truthValueMap.find(*pNegatedItem) != truthValueMap.end())
913  {
914  truthValueMap[*pNegatedItem] = !(bitSet[j]);
915  }
916 
917  delete pNegatedItem;
918  }
919 
920  // now we evaluate the logical expression to see if the result
921  // is true or false
922  if (this->evaluateExpression(truthValueMap) == true)
923  {
924  // the result was true, so this combination is part of the
925  // canonical disjunctive normalform
926  ItemSet tmpSet;
927 
928  for (j = 0; j < jMax; ++j)
929  {
930  CNormalLogicalItem* pItem = new CNormalLogicalItem(itemVector[j]);
931 
932  if (bitSet[j] == false)
933  {
934  pItem->negate();
935  pItem->simplify();
936  }
937 
938  tmpSet.insert(std::make_pair(pItem, false));
939  }
940 
941  tmpAndSets.insert(std::make_pair(tmpSet, false));
942  }
943 
944  ++i;
945  }
946  }
947  else
948  {
949  result = false;
950  }
951  }
952  else
953  {
954  result = false;
955  }
956 
957  return result;
958 }
959 
960 bool CNormalLogical::evaluateExpression(const std::map<CNormalLogicalItem, bool>& truthValueMap) const
961 {
962  bool result = false;
963  ItemSetOfSets::const_iterator outerIt = this->mAndSets.begin(), outerEndit = this->mAndSets.end();
964 
965  while (outerIt != outerEndit)
966  {
967  ItemSet::const_iterator innerIt = outerIt->first.begin(), innerEndit = outerIt->first.end();
968  bool innerResult = true;
969 
970  while (innerIt != innerEndit && innerResult == true)
971  {
972  std::map<CNormalLogicalItem, bool>::const_iterator pos = truthValueMap.find(*(innerIt->first));
973  assert(pos != truthValueMap.end());
974 
975  if (pos != truthValueMap.end())
976  {
977  innerResult = pos->second;
978 
979  if (innerIt->second == true) innerResult = (!innerResult);
980  }
981  else
982  {
983  innerResult = false;
984  }
985 
986  ++innerIt;
987  }
988 
989  if (outerIt->second == true)
990  {
991  innerResult = (!innerResult);
992  }
993 
994  if (innerResult == true)
995  {
996  result = true;
997  break;
998  }
999 
1000  ++outerIt;
1001  }
1002 
1003  return result;
1004 }
1005 
1006 /**
1007  * This methods checks wether there is something like A and !A in a set, if
1008  * such an occurance is found, the whole set is converted to a set with either a false or a true item.
1009  * For or combined items, this would be true, for and combined
1010  * sets, it would be false.
1011  * If there already are sets in the outer set, this set could be eliminated
1012  * altogether.
1013  */
1014 void CNormalLogical::eliminateNullItems(const ItemSetOfSets& source, ItemSetOfSets& target, bool orSet)
1015 {
1016  CNormalLogicalItem neutralItem = CNormalLogicalItem();
1017 
1018  if (orSet == true)
1019  {
1020  // the outer set is or combined, so the items in the inner set are and
1021  // combined and the neutral item is for the outer set is the false item
1022  // and for the innerset it is the true item
1023  neutralItem.setType(CNormalLogicalItem::FALSE);
1024  }
1025  else
1026  {
1027  neutralItem.setType(CNormalLogicalItem::TRUE);
1028  }
1029 
1030  ItemSetOfSets::const_iterator outerIt = source.begin(), outerEndit = source.end();
1031  ItemSetOfSets tmpTarget;
1032  CNormalLogicalItem* pNegatedNeutralItem = new CNormalLogicalItem(neutralItem);
1033  pNegatedNeutralItem->negate();
1034  pNegatedNeutralItem->simplify();
1035  std::pair<CNormalLogicalItem*, bool> pNegatedNeutralItemPair1 = std::make_pair(&neutralItem, false);
1036  std::pair<CNormalLogicalItem*, bool> pNegatedNeutralItemPair2 = std::make_pair(pNegatedNeutralItem, true);
1037 
1038  while (outerIt != outerEndit)
1039  {
1040  ItemSet::const_iterator innerIt = outerIt->first.begin(), innerEndit = outerIt->first.end();
1041  bool eliminate = false;
1042 
1043  while (innerIt != innerEndit)
1044  {
1045  if (outerIt->first.find(pNegatedNeutralItemPair1) != outerIt->first.end() || outerIt->first.find(pNegatedNeutralItemPair2) != outerIt->first.end())
1046  {
1047  eliminate = true;
1048  break;
1049  }
1050 
1051  CNormalLogicalItem* pNegatedItem = new CNormalLogicalItem(*innerIt->first);
1052  pNegatedItem->negate();
1053  std::pair<CNormalLogicalItem*, bool> negatedPair = std::make_pair(pNegatedItem, innerIt->second);
1054  ItemSet::const_iterator pos = outerIt->first.find(negatedPair);
1055 
1056  if (pos != outerIt->first.end())
1057  {
1058  eliminate = true;
1059  delete pNegatedItem;
1060  break;
1061  }
1062 
1063  // also look for the simplified form just in case
1064  pNegatedItem->simplify();
1065  pos = outerIt->first.find(negatedPair);
1066 
1067  if (pos != outerIt->first.end())
1068  {
1069  eliminate = true;
1070  delete pNegatedItem;
1071  break;
1072  }
1073 
1074  delete pNegatedItem;
1075  ++innerIt;
1076  }
1077 
1078  ItemSet tmpSet;
1079 
1080  if (eliminate)
1081  {
1082  CNormalLogicalItem* pTmpItem = new CNormalLogicalItem(neutralItem);
1083 
1084  if (innerIt->second == true)
1085  {
1086  pTmpItem->negate();
1087  }
1088 
1089  // only add simplified elements
1090  pTmpItem->simplify();
1091  tmpSet.insert(std::make_pair(pTmpItem, false));
1092  }
1093  else
1094  {
1095  innerIt = outerIt->first.begin(), innerEndit = outerIt->first.end();
1096 
1097  while (innerIt != innerEndit)
1098  {
1099  CNormalLogicalItem* pNewItem = new CNormalLogicalItem(*innerIt->first);
1100 
1101  if (innerIt->second == true)
1102  {
1103  pNewItem->negate();
1104  }
1105 
1106  pNewItem->simplify();
1107  tmpSet.insert(std::make_pair(pNewItem, false));
1108  ++innerIt;
1109  }
1110 
1111  // remove the neutral item of the inner set if there is more than one item in the
1112  // set
1113  if (tmpSet.size() > 1)
1114  {
1115  // neutralItem is the neutral item for the outer set
1116  // to get the neutral item for the inner set, we have to negate
1117  // the one for the outer set
1118  CNormalLogicalItem* pItem = new CNormalLogicalItem(neutralItem);
1119  pItem->negate();
1120  pItem->simplify();
1121  std::pair<CNormalLogicalItem*, bool> tmpPair = std::make_pair(pItem, false);
1122  ItemSet::const_iterator p = tmpSet.find(tmpPair);
1123 
1124  if (p != tmpSet.end())
1125  {
1126  CNormalLogicalItem* pTmpItem = p->first;
1127  tmpSet.erase(tmpPair);
1128  delete pTmpItem;
1129  }
1130 
1131  delete pItem;
1132  // since all items in tmpSet are simplified, we don't have to
1133  // look for the negated form of pItem with a true flag
1134  }
1135  }
1136 
1137  if (tmpTarget.insert(std::make_pair(tmpSet, outerIt->second)).second == false)
1138  {
1139  // TODO check why this is the case in e.g. test_normalform::test_nested_stepwise_fractions_3levels
1140  // TODO But right now this does not seem to invalidate the results.
1141  cleanSet(tmpSet);
1142  tmpSet.clear();
1143  }
1144 
1145  ++outerIt;
1146  }
1147 
1148  // now we have to do the same thing for the outer set
1149  outerIt = tmpTarget.begin();
1150  outerEndit = tmpTarget.end();
1151 
1152  while (outerIt != outerEndit)
1153  {
1154  const ItemSet& sourceSet = outerIt->first;
1155 
1156  // we can only check for the negated set if there is only one item in
1157  // the set, everything else is to complicated for now
1158  if (sourceSet.size() == 1)
1159  {
1160  if ((sourceSet.begin()->first->getType() == pNegatedNeutralItem->getType() && sourceSet.begin()->second == false) || (sourceSet.begin()->first->getType() == neutralItem.getType() && sourceSet.begin()->second == true))
1161  {
1162  // we can stop here since we now know that the whole set of sets
1163  // is true or false depending on the logical order of the set of
1164  // sets.
1165  cleanSetOfSets(target);
1166  ItemSet neutralSet;
1167  CNormalLogicalItem* pI = new CNormalLogicalItem(neutralItem);
1168  pI->negate();
1169  neutralSet.insert(std::make_pair(pI, false));
1170 
1171  if (target.insert(std::make_pair(neutralSet, false)).second == false)
1172  {
1173  delete pI;
1174  }
1175 
1176  break;
1177  }
1178 
1179  ItemSet tmpSet;
1180  CNormalLogicalItem* pItem = new CNormalLogicalItem(*sourceSet.begin()->first);
1181  pItem->negate();
1182  pItem->simplify();
1183  tmpSet.insert(std::make_pair(pItem, outerIt->second));
1184  std::pair<ItemSet, bool> tmpPair = std::make_pair(tmpSet, false);
1185 
1186  if (tmpTarget.find(tmpPair) != tmpTarget.end())
1187  {
1188  // we can stop here since we now know that the whole set of sets
1189  // is true or false depending on the logical order of the set of
1190  // sets.
1191  cleanSetOfSets(target);
1192  ItemSet neutralSet;
1193  CNormalLogicalItem* pI = new CNormalLogicalItem(neutralItem);
1194  pI->negate();
1195  neutralSet.insert(std::make_pair(pI, false));
1196 
1197  if (target.insert(std::make_pair(neutralSet, false)).second == false)
1198  {
1199  delete pI;
1200  }
1201 
1202  delete pItem;
1203  break;
1204  }
1205  else
1206  {
1207  ItemSet tmpSet2;
1208  copySet(sourceSet, tmpSet2);
1209 
1210  if (target.insert(std::make_pair(tmpSet2, outerIt->second)).second == false)
1211  {
1212  cleanSet(tmpSet2);
1213  tmpSet.clear();
1214  }
1215  }
1216 
1217  delete pItem;
1218  }
1219  else
1220  {
1221  ItemSet tmpSet2;
1222  copySet(sourceSet, tmpSet2);
1223 
1224  if (target.insert(std::make_pair(tmpSet2, outerIt->second)).second == false)
1225  {
1226  cleanSet(tmpSet2);
1227  tmpSet2.clear();
1228  }
1229  }
1230 
1231  ++outerIt;
1232  }
1233 
1234  cleanSetOfSets(tmpTarget);
1235  delete pNegatedNeutralItem;
1236 
1237  if (target.size() > 1)
1238  {
1239  // remove the neutral element from the outer set
1240  ItemSet neutralSet;
1241  CNormalLogicalItem* pI = new CNormalLogicalItem(neutralItem);
1242  neutralSet.insert(std::make_pair(pI, false));
1243  std::pair<ItemSet, bool> neutralPair = std::make_pair(neutralSet, false);
1244  ItemSetOfSets::const_iterator pos = target.find(neutralPair);
1245 
1246  if (pos != target.end())
1247  {
1248  CNormalLogicalItem* pTmpItem = pos->first.begin()->first;
1249  target.erase(neutralPair);
1250  delete pTmpItem;
1251  }
1252 
1253  pI->negate();
1254  neutralPair = std::make_pair(neutralSet, true);
1255  pos = target.find(neutralPair);
1256 
1257  if (pos != target.end())
1258  {
1259  CNormalLogicalItem* pTmpItem = pos->first.begin()->first;
1260  target.erase(neutralPair);
1261  delete pTmpItem;
1262  }
1263 
1264  delete pI;
1265  }
1266 }
1267 
1268 #ifdef COPASI_DEBUG
1269 
1270 void CNormalLogical::printSetOfSets(const ItemSetOfSets& set)
1271 {
1272  ItemSetOfSets::const_iterator outerIt = set.begin(), outerEndit = set.end();
1273 
1274  while (outerIt != outerEndit)
1275  {
1276  ItemSet::const_iterator innerIt = outerIt->first.begin(), innerEndit = outerIt->first.end();
1277 
1278  while (innerIt != innerEndit)
1279  {
1280  std::cout << innerIt->first->toString() << " ^ ";
1281  ++innerIt;
1282  }
1283 
1284  std::cout << std::endl;
1285  ++outerIt;
1286  }
1287 }
1288 
1289 void CNormalLogical::printSetSizes(const ItemSetOfSets& set)
1290 {
1291  ItemSetOfSets::const_iterator outerIt = set.begin(), outerEndit = set.end();
1292  std::cout << "Number of Sets: " << set.size() << std::endl;
1293 
1294  while (outerIt != outerEndit)
1295  {
1296  std::cout << " Number of elements in set: " << outerIt->first.size() << std::endl;
1297  ++outerIt;
1298  }
1299 }
1300 
1301 void CNormalLogical::printSetElement(const ItemSetOfSets& set, unsigned int index1, unsigned int index2)
1302 {
1303  if (index1 >= set.size()) return;
1304 
1305  ItemSetOfSets::const_iterator outerIt = set.begin();
1306  unsigned int i = 0;
1307 
1308  while (i < index1)
1309  {
1310  ++i;
1311  ++outerIt;
1312  }
1313 
1314  if (index2 >= outerIt->first.size()) return;
1315 
1316  i = 0;
1317  ItemSet::const_iterator innerIt = outerIt->first.begin();
1318 
1319  while (i < index2)
1320  {
1321  ++i;
1322  ++innerIt;
1323  }
1324 
1325  std::cout << innerIt->first->toString();
1326 }
1327 #endif // COPASI_DEBUG
static bool negateSets(const TemplateSet< TYPE > &source, TemplateSet< TYPE > &target)
ChoiceSetOfSets & getChoices()
virtual std::string toString() const
static void eliminateNullItems(const ItemSetOfSets &source, ItemSetOfSets &target, bool orSet)
CNormalLogical & operator=(const CNormalLogical &src)
static void cleanSetOfSets(TemplateSetOfSets< TYPE > &s)
bool evaluateExpression(const std::map< CNormalLogicalItem, bool > &truthValueMap) const
virtual bool simplify()
C_LOGICAL logical
Definition: f2c.h:18
TemplateSetOfSets< CNormalLogicalItem > ItemSetOfSets
ItemSetOfSets mAndSets
bool isNegated() const
bool generateCanonicalDNF(ItemSetOfSets &tmpAndSet) const
virtual std::string toString() const
virtual ~CNormalLogical()
void setAndSets(const ItemSetOfSets &set)
static bool negateSetOfSets(const TemplateSetOfSets< TYPE > &source, TemplateSetOfSets< TYPE > &target)
static bool convertAndOrToOrAnd(const TemplateSetOfSets< TYPE > &source, TemplateSetOfSets< TYPE > &target)
void setChoices(const ChoiceSetOfSets &set)
static void cleanSet(const TemplateSet< TYPE > &s)
bool isEqual(const std::pair< TemplateSet< TYPE >, bool > &lhs, const std::pair< TemplateSet< TYPE >, bool > &rhs) const
static void copySetOfSets(const TemplateSetOfSets< TYPE > &source, TemplateSetOfSets< TYPE > &target)
bool operator<(const CNormalLogical &rhs) const
void setIsNegated(bool negate)
virtual CNormalBase * copy() const
static void copySet(const TemplateSet< TYPE > &source, TemplateSet< TYPE > &target)
std::ostream & operator<<(std::ostream &os, const CNormalLogical &logical)
bool operator==(const CNormalLogical &rhs) const
ChoiceSetOfSets mChoices
ItemSetOfSets & getAndSets()