diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 18:58:54 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 18:58:54 -0400 |
commit | 87b9af34d7864044aa70720cfd32bf259750772b (patch) | |
tree | fc2a9430a963fc575e165872f454165bdbeff143 /src/theory | |
parent | 63437aec44747fb9ad0ab6264ae5e4bbf3dc0e5b (diff) | |
parent | 2624b945cbb1dd92efea28220fb38f5ebaf0b66a (diff) |
Merge branch '1.4.x'
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 51 |
1 files changed, 28 insertions, 23 deletions
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 60b89451a..4125fd193 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -599,33 +599,38 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements if( !alreadyCalculated ) { Kind k = setterm.getKind(); - unsigned numChildren = setterm.getNumChildren(); Elements cur; - if(numChildren == 2) { + + switch(k) { + case kind::UNION: { const Elements& left = getElements(setterm[0], settermElementsMap); const Elements& right = getElements(setterm[1], settermElementsMap); - switch(k) { - case kind::UNION: - if(left.size() >= right.size()) { - cur = left; cur.insert(right.begin(), right.end()); - } else { - cur = right; cur.insert(left.begin(), left.end()); - } - break; - case kind::INTERSECTION: - std::set_intersection(left.begin(), left.end(), right.begin(), right.end(), - std::inserter(cur, cur.begin()) ); - break; - case kind::SETMINUS: - std::set_difference(left.begin(), left.end(), right.begin(), right.end(), - std::inserter(cur, cur.begin()) ); - break; - default: - Unhandled(); + if(left.size() >= right.size()) { + cur = left; cur.insert(right.begin(), right.end()); + } else { + cur = right; cur.insert(left.begin(), left.end()); } - } else { - Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM, - (std::string("Expect variable or UF got ") + kindToString(k)).c_str() ); + break; + } + case kind::INTERSECTION: { + const Elements& left = getElements(setterm[0], settermElementsMap); + const Elements& right = getElements(setterm[1], settermElementsMap); + std::set_intersection(left.begin(), left.end(), right.begin(), right.end(), + std::inserter(cur, cur.begin()) ); + break; + } + case kind::SETMINUS: { + const Elements& left = getElements(setterm[0], settermElementsMap); + const Elements& right = getElements(setterm[1], settermElementsMap); + std::set_difference(left.begin(), left.end(), right.begin(), right.end(), + std::inserter(cur, cur.begin()) ); + break; + } + default: + Assert(theory::kindToTheoryId(k) != theory::THEORY_SETS, + (std::string("Kind belonging to set theory not explicitly handled: ") + kindToString(k)).c_str()); + // Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM, + // (std::string("Expect variable or UF got ") + kindToString(k)).c_str() ); /* assign emptyset, which is default */ } |