Lines Matching refs:PresburgerSet
29 static void testUnionAtPoints(const PresburgerSet &s, const PresburgerSet &t, in testUnionAtPoints()
31 PresburgerSet unionSet = s.unionSet(t); in testUnionAtPoints()
42 static void testIntersectAtPoints(const PresburgerSet &s, in testIntersectAtPoints()
43 const PresburgerSet &t, in testIntersectAtPoints()
45 PresburgerSet intersection = s.intersect(t); in testIntersectAtPoints()
56 static void testSubtractAtPoints(const PresburgerSet &s, const PresburgerSet &t, in testSubtractAtPoints()
58 PresburgerSet diff = s.subtract(t); in testSubtractAtPoints()
72 static void testComplementAtPoints(const PresburgerSet &s, in testComplementAtPoints()
74 PresburgerSet complement = s.complement(); in testComplementAtPoints()
90 static PresburgerSet makeSetFromPoly(unsigned numDims, in makeSetFromPoly()
92 PresburgerSet set = in makeSetFromPoly()
93 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(numDims)); in makeSetFromPoly()
100 PresburgerSet setA = parsePresburgerSetFromPolyStrings( in TEST()
112 PresburgerSet setB = parsePresburgerSetFromPolyStrings( in TEST()
129 EXPECT_TRUE(PresburgerSet(parsePoly("(x) : (x - 2*(x floordiv 2) == 0)")) in TEST()
134 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
139 testUnionAtPoints(PresburgerSet::getUniverse(PresburgerSpace::getSetSpace(1)), in TEST()
143 testUnionAtPoints(PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(1)), in TEST()
147 testUnionAtPoints(PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(1)), in TEST()
148 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace(1)), in TEST()
152 testUnionAtPoints(PresburgerSet::getUniverse(PresburgerSpace::getSetSpace(1)), in TEST()
153 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace(1)), in TEST()
157 testUnionAtPoints(PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), in TEST()
158 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), in TEST()
163 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
169 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))), set, in TEST()
174 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), set, in TEST()
179 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), in TEST()
180 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))), in TEST()
185 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))), in TEST()
186 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), in TEST()
191 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))), in TEST()
192 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))), in TEST()
348 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))), in TEST()
353 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))), in TEST()
375 PresburgerSet universe = in TEST()
376 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1))); in TEST()
377 PresburgerSet emptySet = in TEST()
378 PresburgerSet::getEmpty(PresburgerSpace::getSetSpace((1))); in TEST()
379 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
417 PresburgerSet square = parsePresburgerSetFromPolyStrings( in TEST()
419 PresburgerSet rect = parsePresburgerSetFromPolyStrings( in TEST()
422 PresburgerSet universeRect = square.unionSet(square.complement()); in TEST()
423 PresburgerSet universeSquare = rect.unionSet(rect.complement()); in TEST()
430 void expectEqual(const PresburgerSet &s, const PresburgerSet &t) { in expectEqual()
438 void expectEmpty(const PresburgerSet &s) { EXPECT_TRUE(s.isIntegerEmpty()); } in expectEmpty()
442 PresburgerSet evens{parsePoly("(x) : (x - 2 * (x floordiv 2) == 0)")}; in TEST()
445 PresburgerSet odds{parsePoly("(x) : (x - 2 * (x floordiv 2) - 1 == 0)")}; in TEST()
448 PresburgerSet multiples3{parsePoly("(x) : (x - 3 * (x floordiv 3) == 0)")}; in TEST()
451 PresburgerSet multiples6{parsePoly("(x) : (x - 6 * (x floordiv 6) == 0)")}; in TEST()
454 expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds))); in TEST()
457 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1)))); in TEST()
463 PresburgerSet setA{parsePoly("(x) : (-x >= 0)")}; in TEST()
464 PresburgerSet setB{parsePoly("(x) : (x floordiv 2 - 4 >= 0)")}; in TEST()
482 PresburgerSet evens{ in TEST()
486 PresburgerSet odds{ in TEST()
490 PresburgerSet multiples3{ in TEST()
494 PresburgerSet multiples6{ in TEST()
498 expectEmpty(PresburgerSet(evens).intersect(PresburgerSet(odds))); in TEST()
501 PresburgerSet::getUniverse(PresburgerSpace::getSetSpace((1)))); in TEST()
507 PresburgerSet evensDefByIneq{ in TEST()
509 expectEqual(evens, PresburgerSet(evensDefByIneq)); in TEST()
542 PresburgerSet triangle2{parsePolyAndMakeLocals("(x,y) : (y >= 0, " in TEST()
546 PresburgerSet zeroToThirteen{parsePoly("(x) : (13 - x >= 0, x >= 0)")}; in TEST()
547 PresburgerSet fifteen{parsePoly("(x) : (x - 15 == 0)")}; in TEST()
563 void expectCoalesce(size_t expectedNumPoly, const PresburgerSet &set) { in expectCoalesce()
564 PresburgerSet newSet = set.coalesce(); in expectCoalesce()
570 PresburgerSet set = makeSetFromPoly(0, {}); in TEST()
575 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
581 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
587 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
593 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
599 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
605 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
611 PresburgerSet set = in TEST()
617 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
623 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
629 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
638 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
644 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
650 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
659 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
668 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
677 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
686 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
695 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
704 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
713 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
722 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
731 PresburgerSet set = in TEST()
741 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
752 PresburgerSet set = parsePresburgerSetFromPolyStrings( in TEST()
763 PresburgerSet set = in TEST()
772 PresburgerSet set = in TEST()
782 expectComputedVolumeIsValidOverapprox(const PresburgerSet &set, in expectComputedVolumeIsValidOverapprox()
791 PresburgerSet diamond( in TEST()
799 PresburgerSet shiftedDiamond(parsePoly( in TEST()
807 PresburgerSet biggerDiamond(parsePoly( in TEST()
826 PresburgerSet unbounded(parsePoly("(x, y) : (2*x - y >= 0, y - 3*x >= 0)")); in TEST()
852 void testComputeRepr(IntegerPolyhedron poly, const PresburgerSet &expected, in testComputeRepr()
880 PresburgerSet(parsePoly({"(x) : (x - 3*(x floordiv 3) == 0)"})), in TEST()
885 PresburgerSet set1 = in TEST()
887 PresburgerSet set2 = in TEST()
890 PresburgerSet set3 = in TEST()
893 PresburgerSet result = set1.subtract(set2); in TEST()
901 PresburgerSet subtractSelf = set1.subtract(set1); in TEST()