PresburgerRelation.cpp Source File (original) (raw)

15 #include "llvm/ADT/STLExtras.h"

16 #include "llvm/ADT/SmallBitVector.h"

17 #include "llvm/ADT/SmallVector.h"

18 #include "llvm/Support/LogicalResult.h"

19 #include "llvm/Support/raw_ostream.h"

20 #include

21 #include

22 #include

23 #include

24 #include

26 using namespace mlir;

27 using namespace presburger;

30 : space(disjunct.getSpaceWithoutLocals()) {

32 }

38 disjunct.setSpaceExceptLocals(space);

39 }

42 unsigned num) {

44 cs.insertVar(kind, pos, num);

46 }

49 unsigned num, VarKind dstKind,

50 unsigned dstPos) {

52 "srcKind/dstKind cannot be local");

53 assert(srcKind != dstKind && "cannot convert variables to the same kind");

55 "invalid range for source variables");

57 "invalid position for destination variables");

62 disjunct.convertVarKind(srcKind, srcPos, srcPos + num, dstKind, dstPos);

63 }

67 }

71 }

74 assert(index < disjuncts.size() && "index out of bounds!");

76 }

83 }

93 return;

97 return;

98 }

100 return;

101

103 return;

106 return;

107 }

108

111 }

112

113

119 return result;

120 }

121

122

126 });

127 }

128

133 return result;

134 }

135

138 }

139

140

141

142

143

144

145

146

150

151

152

154 return *this;

155

157 return set;

158

163 if (!intersection.isEmpty())

165 }

166 }

167 return result;

168 }

169

173 "Range of `this` must be compatible with range of `set`");

174

178 }

179

183 "Domain of `this` must be compatible with range of `set`");

184

189 }

190

195 return result;

196 }

197

202 return result;

203 }

204

207 cs.inverse();

208

211 }

212

214 assert(getSpace().getRangeSpace().isCompatible(

216 "Range of `this` should be compatible with domain of `rel`");

217

224 composition.compose(csB);

225 if (!composition.isEmpty())

227 }

228 }

229 *this = result;

230 }

231

233 assert(getSpace().getDomainSpace().isCompatible(

235 "Domain of `this` should be compatible with domain of `rel`");

236

240 }

241

244 }

245

247 bool isMin) {

253 if (isMin) {

254 s = cs.findSymbolicIntegerLexMin();

256 } else {

257 s = cs.findSymbolicIntegerLexMax();

259 }

261 }

262 return result;

263 }

264

267 }

268

271 }

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

290 "idx out of bounds!");

292 return llvm::to_vector<8>(rel.getInequality(idx));

293

296

297 if (idx % 2 == 0)

298 return llvm::to_vector<8>(eqCoeffs);

300 }

301

304 return *this;

305

306

309 result.unionInPlace(disjunct.computeReprWithOnlyDivLocals());

310 return result;

311 }

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

328

329

330

331

332

333

334

335

336

337

338

339

340

341

342

343

344

350

353

354

355

357

361

362

363

364

365

366 struct Frame {

367

368 unsigned simplexSnapshot;

369

371

373

374

376

377

378 std::optional lastIneqProcessed;

379

380

381 Frame(unsigned simplexSnapshot,

384 std::optional lastIneqProcessed = std::nullopt)

385 : simplexSnapshot(simplexSnapshot), bCounts(bCounts), sI(sI),

386 ineqsToProcess(ineqsToProcess), lastIneqProcessed(lastIneqProcessed) {

387 }

388 };

390

391

392

393 unsigned level = 1;

394 while (level > 0) {

396

398 level = frames.size();

399 continue;

400 }

401

402 if (level > frames.size()) {

403

405

406

408

409

410

411

412

414

415 unsigned initialSnapshot = simplex.getSnapshot();

416

417

418

419

420

422

423

424

425

426

427

430

431

432

437 i < e; ++i) {

438 assert(

439 repr[i] &&

440 "Subtraction is not supported when a representation of the local "

441 "variables of the subtrahend cannot be found!");

442

444 unsigned lb = repr[i].repr.inequalityPair.lowerBoundIdx;

445 unsigned ub = repr[i].repr.inequalityPair.upperBoundIdx;

446

449

450 assert(lb != ub &&

451 "Upper and lower bounds must be different inequalities!");

452 canIgnoreIneq[lb] = true;

453 canIgnoreIneq[ub] = true;

454 } else {

456 "ReprKind isn't inequality so should be equality");

457

458

459

460

461

462

463

464

465

466

467

468

469

470

471

472

479 }

480 }

481

483 unsigned numLocalsAdded =

486

487 unsigned snapshotBeforeIntersect = simplex.getSnapshot();

489

491

492

493

495 simplex.rollback(initialSnapshot);

496

497

498

499

500

501 frames.emplace_back(Frame{initialSnapshot, initBCounts, sI});

502 ++level;

503 continue;

504 }

505

506

507 unsigned totalNewSimplexInequalities =

509

510

511

512

513

514

515

516

517

518

519

520

521

522 simplex.detectRedundant(offset, totalNewSimplexInequalities);

523 for (unsigned j = 0; j < totalNewSimplexInequalities; j++)

525 simplex.rollback(snapshotBeforeIntersect);

526

528 ineqsToProcess.reserve(totalNewSimplexInequalities);

529 for (unsigned i = 0; i < totalNewSimplexInequalities; ++i)

530 if (!canIgnoreIneq[i])

531 ineqsToProcess.emplace_back(i);

532

533 if (ineqsToProcess.empty()) {

534

535 level = frames.size();

536 continue;

537 }

538

539 unsigned simplexSnapshot = simplex.getSnapshot();

541 frames.emplace_back(Frame{simplexSnapshot, bCounts, sI, ineqsToProcess});

542

543

544 }

545

546

547

548

549 if (level == frames.size()) {

550 Frame &frame = frames.back();

551 if (frame.lastIneqProcessed) {

552

553

554

555

556

557

558

559 simplex.rollback(frame.simplexSnapshot);

565 }

566

567 if (frame.ineqsToProcess.empty()) {

568

569 frames.pop_back();

570 level = frames.size();

571 continue;

572 }

573

574

576 frame.simplexSnapshot = simplex.getSnapshot();

577

578 unsigned idx = frame.ineqsToProcess.back();

583

584 frame.ineqsToProcess.pop_back();

585 frame.lastIneqProcessed = idx;

586 ++level;

587 continue;

588 }

589 }

590

591

593

594 return result;

595 }

596

597

600 }

601

602

603

608

609

610

612 return result;

613

614

617 return result;

618 }

619

620

621

622

625 }

626

627

631 }

632

635 return false;

636

638 return false;

639

640

641

642 for (unsigned int i = 0, n = getNumDisjuncts(); i < n; ++i) {

644 return false;

645 }

646 return true;

647 }

648

649

650

651

652

655 if (disjunct.getNumConstraints() == 0)

656 return true;

657 }

658 return false;

659 }

660

663 }

664

665

668 }

669

670

671

673

675 }

676

679

682 disjunct.findIntegerSample()) {

683 sample = std::move(*opt);

684 return true;

685 }

686 }

687 return false;

688 }

689

691 assert(getNumSymbolVars() == 0 && "Symbols are not yet supported!");

692

693

694 DynamicAPInt result(0);

696 std::optional volume = disjunct.computeVolume();

697 if (!volume)

698 return {};

699 result += *volume;

700 }

701 return result;

702 }

703

704

705

706

707

708

709

711

712 public:

713

715

716

718

719 private:

720

722

723

724

726

728

729

730

732

733

734

737

740

741

742

743

745

746

747

748

749 void addCoalescedDisjunct(unsigned i, unsigned j,

751

752

753

754

755

756

757

758

759

760

761

762

763 LogicalResult coalescePairCutCase(unsigned i, unsigned j);

764

765

766

767

769

770

771

772

773

775

776

777

778 void eraseDisjunct(unsigned i);

779

780

781

782

783

784

785 LogicalResult coalescePair(unsigned i, unsigned j);

786 };

787

788

789

791

793

795

796 for (unsigned i = 0; i < disjuncts.size();) {

797 disjuncts[i].removeRedundantConstraints();

798 Simplex simp(disjuncts[i]);

800 disjuncts[i] = disjuncts[disjuncts.size() - 1];

801 disjuncts.pop_back();

802 continue;

803 }

804 ++i;

805 simplices.emplace_back(simp);

806 }

807 }

808

809

811

812

813

814

815 for (unsigned i = 0; i < disjuncts.size();) {

816

817

818

819 bool broken = false;

820 for (unsigned j = 0, e = disjuncts.size(); j < e; ++j) {

821 negEqs.clear();

822 redundantIneqsA.clear();

823 redundantIneqsB.clear();

824 cuttingIneqsA.clear();

825 cuttingIneqsB.clear();

826 if (i == j)

827 continue;

828 if (coalescePair(i, j).succeeded()) {

829 broken = true;

830 break;

831 }

832 }

833

834

835

836

837 if (!broken)

838 ++i;

839 }

840

844

845 return newSet;

846 }

847

848

849

850

857 });

858 }

859

860 void SetCoalescer::addCoalescedDisjunct(unsigned i, unsigned j,

862 assert(i != j && "The indices must refer to different disjuncts");

863 unsigned n = disjuncts.size();

864 if (j == n - 1) {

865

866

867

868 disjuncts[i] = disjuncts[n - 2];

869 disjuncts.pop_back();

870 disjuncts[n - 2] = disjunct;

871 disjuncts[n - 2].removeRedundantConstraints();

872

873 simplices[i] = simplices[n - 2];

874 simplices.pop_back();

875 simplices[n - 2] = Simplex(disjuncts[n - 2]);

876

877 } else {

878

879

880

881

882

883 disjuncts[i] = disjuncts[n - 1];

884 disjuncts[j] = disjuncts[n - 2];

885 disjuncts.pop_back();

886 disjuncts[n - 2] = disjunct;

887 disjuncts[n - 2].removeRedundantConstraints();

888

889 simplices[i] = simplices[n - 1];

890 simplices[j] = simplices[n - 2];

891 simplices.pop_back();

892 simplices[n - 2] = Simplex(disjuncts[n - 2]);

893 }

894 }

895

896

897

898

899

900

901

902

903

904

905

906

907

908

909

910

911

912 LogicalResult SetCoalescer::coalescePairCutCase(unsigned i, unsigned j) {

913

914

915 Simplex &simp = simplices[i];

918 return !isFacetContained(curr, simp);

919 }))

920 return failure();

922

924 newSet.addInequality(curr);

925

927 newSet.addInequality(curr);

928

929 addCoalescedDisjunct(i, j, newSet);

930 return success();

931 }

932

936 if (type == Simplex::IneqType::Redundant)

937 redundantIneqsB.emplace_back(ineq);

938 else if (type == Simplex::IneqType::Cut)

939 cuttingIneqsB.emplace_back(ineq);

940 else

941 return failure();

942 return success();

943 }

944

947 if (typeInequality(eq, simp).failed())

948 return failure();

951 return typeInequality(inv, simp);

952 }

953

954 void SetCoalescer::eraseDisjunct(unsigned i) {

955 assert(simplices.size() == disjuncts.size() &&

956 "simplices and disjuncts must be equally as long");

957 disjuncts[i] = disjuncts.back();

958 disjuncts.pop_back();

959 simplices[i] = simplices.back();

960 simplices.pop_back();

961 }

962

963 LogicalResult SetCoalescer::coalescePair(unsigned i, unsigned j) {

964

967

968

969

971 return failure();

972 Simplex &simpA = simplices[i];

973 Simplex &simpB = simplices[j];

974

975

976

977

978

979

981 if (typeInequality(a.getInequality(k), simpB).failed())

982 return failure();

983

985 if (typeEquality(a.getEquality(k), simpB).failed())

986 return failure();

987

988 std::swap(redundantIneqsA, redundantIneqsB);

989 std::swap(cuttingIneqsA, cuttingIneqsB);

990

992 if (typeInequality(b.getInequality(k), simpA).failed())

993 return failure();

994

996 if (typeEquality(b.getEquality(k), simpA).failed())

997 return failure();

998

999

1000

1001 if (cuttingIneqsA.empty()) {

1002 eraseDisjunct(j);

1003 return success();

1004 }

1005

1006

1007 if (coalescePairCutCase(i, j).succeeded())

1008 return success();

1009

1010

1011 std::swap(redundantIneqsA, redundantIneqsB);

1012 std::swap(cuttingIneqsA, cuttingIneqsB);

1013

1014

1015

1016 if (cuttingIneqsA.empty()) {

1017 eraseDisjunct(i);

1018 return success();

1019 }

1020

1021

1022 return coalescePairCutCase(j, i);

1023 }

1024

1027 }

1028

1032 });

1033 }

1034

1042 }

1043 return result;

1044 }

1045

1049 });

1050 }

1051

1053 os << "Number of Disjuncts: " << getNumDisjuncts() << "\n";

1055 disjunct.print(os);

1056 os << '\n';

1057 }

1058 }

1059

1061

1065 return result;

1066 }

1067

1070 }

1071

1074

1077

1080 }

1081

1084 }

1085

1088 }

1089

1092 }

1093

1096 }

union mlir::linalg::@1203::ArityGroupAndKind::Kind kind

static SymbolicLexOpt findSymbolicIntegerLexOpt(const PresburgerRelation &rel, bool isMin)

static SmallVector< DynamicAPInt, 8 > getIneqCoeffsFromIdx(const IntegerRelation &rel, unsigned idx)

Return the coefficients of the ineq in rel specified by idx.

static PresburgerRelation getSetDifference(IntegerRelation b, const PresburgerRelation &s)

Return the set difference b \ s.

Class storing division representation of local variables of a constraint system.

DynamicAPInt & getDenom(unsigned i)

MutableArrayRef< DynamicAPInt > getDividend(unsigned i)

An IntegerPolyhedron represents the set of points from a PresburgerSpace that satisfy a list of affin...

static IntegerPolyhedron getUniverse(const PresburgerSpace &space)

Return a system with no constraints, i.e., one which is satisfied by all points.

An IntegerRelation represents the set of points from a PresburgerSpace that satisfy a list of affine ...

void compose(const IntegerRelation &rel)

Let the relation this be R1, and the relation rel be R2.

PresburgerSpace getSpaceWithoutLocals() const

Returns a copy of the space without locals.

void truncate(const CountsSnapshot &counts)

CountsSnapshot getCounts() const

std::optional< SmallVector< DynamicAPInt, 8 > > containsPointNoLocal(ArrayRef< DynamicAPInt > point) const

Given the values of non-local vars, return a satisfying assignment to the local if one exists,...

ArrayRef< DynamicAPInt > getInequality(unsigned idx) const

bool isEmptyByGCDTest() const

Runs the GCD test on all equality constraints.

void simplify()

Simplify the constraint system by removing canonicalizing constraints and removing redundant constrai...

void removeDuplicateDivs()

void print(raw_ostream &os) const

bool isIntegerEmpty() const

Returns true if the set of constraints is found to have no solution, false if a solution exists.

IntegerRelation intersect(IntegerRelation other) const

Return the intersection of the two relations.

static IntegerRelation getUniverse(const PresburgerSpace &space)

Return a system with no constraints, i.e., one which is satisfied by all points.

unsigned getNumLocalVars() const

bool isObviouslyEmpty() const

Performs GCD checks and invalid constraint checks.

bool isEmpty() const

Checks for emptiness by performing variable elimination on all variables, running the GCD test on eac...

DivisionRepr getLocalReprs(std::vector< MaybeLocalRepr > *repr=nullptr) const

Returns a DivisonRepr representing the division representation of local variables in the constraint s...

bool hasOnlyDivLocals() const

Check whether all local ids have a division representation.

void addInequality(ArrayRef< DynamicAPInt > inEq)

Adds an inequality (>= 0) from the coefficients specified in inEq.

unsigned mergeLocalVars(IntegerRelation &other)

Adds additional local vars to the sets such that they both have the union of the local vars in each s...

ArrayRef< DynamicAPInt > getEquality(unsigned idx) const

unsigned getNumInequalities() const

const PresburgerSpace & getSpace() const

Returns a reference to the underlying space.

unsigned getNumEqualities() const

unsigned getVarKindOffset(VarKind kind) const

Return the index at which the specified kind of vars starts.

This class represents a piece-wise MultiAffineFunction.

PWMAFunction unionLexMax(const PWMAFunction &func)

PWMAFunction unionLexMin(const PWMAFunction &func)

Return a function defined on the union of the domains of this and func, such that when only one of th...

A PresburgerRelation represents a union of IntegerRelations that live in the same PresburgerSpace wit...

unsigned getNumSymbolVars() const

void setSpace(const PresburgerSpace &oSpace)

Set the space to oSpace.

unsigned getNumRangeVars() const

PresburgerRelation intersect(const PresburgerRelation &set) const

Return the intersection of this set and the given set.

bool hasOnlyDivLocals() const

Check whether all local ids in all disjuncts have a div representation.

bool containsPoint(ArrayRef< DynamicAPInt > point) const

Return true if the set contains the given point, and false otherwise.

PresburgerRelation subtract(const PresburgerRelation &set) const

Return the set difference of this set and the given set, i.e., return this \ set.

friend class SetCoalescer

PresburgerRelation(const IntegerRelation &disjunct)

PresburgerSet getRangeSet() const

Return a set corresponding to the range of the relation.

bool isConvexNoLocals() const

Return true if the set is consist of a single disjunct, without any local variables,...

PresburgerRelation computeReprWithOnlyDivLocals() const

Compute an equivalent representation of the same relation, such that all local ids in all disjuncts h...

bool isSubsetOf(const PresburgerRelation &set) const

Return true if this set is a subset of the given set, and false otherwise.

unsigned getNumDomainVars() const

bool isIntegerEmpty() const

Return true if all the sets in the union are known to be integer empty false otherwise.

PresburgerRelation intersectRange(const PresburgerSet &set) const

Return the range intersection of the given set with this relation.

void unionInPlace(const IntegerRelation &disjunct)

Mutate this set, turning it into the union of this set and the given disjunct.

std::optional< DynamicAPInt > computeVolume() const

Compute an overapproximation of the number of integer points in the disjunct.

void convertVarKind(VarKind srcKind, unsigned srcPos, unsigned num, VarKind dstKind, unsigned dstPos)

Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of t...

PresburgerRelation intersectDomain(const PresburgerSet &set) const

Return the domain intersection of the given set with this relation.

bool isEqual(const PresburgerRelation &set) const

Return true if this set is equal to the given set, and false otherwise.

static PresburgerRelation getEmpty(const PresburgerSpace &space)

Return an empty set of the specified type that contains no points.

void applyDomain(const PresburgerRelation &rel)

Apply the domain of given relation rel to this relation.

unsigned getNumDisjuncts() const

Return the number of disjuncts in the union.

void applyRange(const PresburgerRelation &rel)

Same as compose, provided for uniformity with applyDomain.

bool findIntegerSample(SmallVectorImpl< DynamicAPInt > &sample)

Find an integer sample from the given set.

bool isObviouslyEmpty() const

Return true if there is no disjunct, false otherwise.

bool isObviouslyUniverse() const

Return true if the set is known to have one unconstrained disjunct, false otherwise.

PresburgerRelation coalesce() const

Simplifies the representation of a PresburgerRelation.

static PresburgerRelation getUniverse(const PresburgerSpace &space)

Return a universe set of the specified type that contains all points.

const IntegerRelation & getDisjunct(unsigned index) const

Return the disjunct at the specified index.

ArrayRef< IntegerRelation > getAllDisjuncts() const

Return a reference to the list of disjuncts.

SmallVector< IntegerRelation, 2 > disjuncts

The list of disjuncts that this set is the union of.

PresburgerRelation simplify() const

Simplify each disjunct, canonicalizing each disjunct and removing redundencies.

void compose(const PresburgerRelation &rel)

Compose this relation with the given relation rel in-place.

const PresburgerSpace & getSpace() const

void print(raw_ostream &os) const

Print the set's internal state.

void inverse()

Invert the relation, i.e.

PresburgerSet getDomainSet() const

Return a set corresponding to the domain of the relation.

SymbolicLexOpt findSymbolicIntegerLexMax() const

Compute the symbolic integer lexmax of the relation, i.e.

void insertVarInPlace(VarKind kind, unsigned pos, unsigned num=1)

PresburgerRelation unionSet(const PresburgerRelation &set) const

Return the union of this set and the given set.

bool isObviouslyEqual(const PresburgerRelation &set) const

Perform a quick equality check on this and other.

SymbolicLexOpt findSymbolicIntegerLexMin() const

Compute the symbolic integer lexmin of the relation, i.e.

bool isFullDim() const

Return whether the given PresburgerRelation is full-dimensional.

PresburgerRelation complement() const

Return the complement of this set.

PresburgerSet intersect(const PresburgerRelation &set) const

PresburgerSet(const IntegerPolyhedron &disjunct)

Create a set from a relation.

PresburgerSet unionSet(const PresburgerRelation &set) const

These operations are the same as the ones in PresburgeRelation, they just forward the arguement and r...

PresburgerSet subtract(const PresburgerRelation &set) const

static PresburgerSet getEmpty(const PresburgerSpace &space)

Return an empty set of the specified type that contains no points.

static PresburgerSet getUniverse(const PresburgerSpace &space)

Return a universe set of the specified type that contains all points.

PresburgerSet coalesce() const

PresburgerSet complement() const

PresburgerSpace is the space of all possible values of a tuple of integer valued variables/variables.

PresburgerSpace getRangeSpace() const

unsigned getNumVarKind(VarKind kind) const

Get the number of vars of the specified kind.

PresburgerSpace getDomainSpace() const

Get the domain/range space of this space.

void convertVarKind(VarKind srcKind, unsigned srcPos, unsigned num, VarKind dstKind, unsigned dstPos)

Converts variables of the specified kind in the column range [srcPos, srcPos + num) to variables of t...

unsigned getNumLocalVars() const

bool isCompatible(const PresburgerSpace &other) const

Returns true if both the spaces are compatible i.e.

static PresburgerSpace getRelationSpace(unsigned numDomain=0, unsigned numRange=0, unsigned numSymbols=0, unsigned numLocals=0)

unsigned insertVar(VarKind kind, unsigned pos, unsigned num=1)

Insert num variables of the specified kind at position pos.

bool isEmpty() const

Returns true if the tableau is empty (has conflicting constraints), false otherwise.

void appendVariable(unsigned count=1)

Add new variables to the end of the list of variables.

void intersectIntegerRelation(const IntegerRelation &rel)

Add all the constraints from the given IntegerRelation.

unsigned getSnapshot() const

Get a snapshot of the current state.

void addEquality(ArrayRef< DynamicAPInt > coeffs)

Add an equality to the tableau.

void rollback(unsigned snapshot)

Rollback to a snapshot. This invalidates all later snapshots.

unsigned getNumConstraints() const

Returns the number of constraints in the tableau.

Takes a snapshot of the simplex state on construction and rolls back to the snapshot on destruction.

The Simplex class uses the Normal pivot rule and supports integer emptiness checks as well as detecti...

bool isMarkedRedundant(unsigned constraintIndex) const

Returns whether the specified constraint has been marked as redundant.

IneqType findIneqType(ArrayRef< DynamicAPInt > coeffs)

Returns the type of the inequality with coefficients coeffs.

bool isRedundantInequality(ArrayRef< DynamicAPInt > coeffs)

Check if the specified inequality already holds in the polytope.

void addInequality(ArrayRef< DynamicAPInt > coeffs) final

Add an inequality to the tableau.

void detectRedundant(unsigned offset, unsigned count)

Finds a subset of constraints that is redundant, i.e., such that the set of solutions does not change...

The SetCoalescer class contains all functionality concerning the coalesce heuristic.

SetCoalescer(const PresburgerRelation &s)

Construct a SetCoalescer from a PresburgerSet.

PresburgerRelation coalesce()

Simplifies the representation of a PresburgerSet.

SmallVector< DynamicAPInt, 8 > getNegatedCoeffs(ArrayRef< DynamicAPInt > coeffs)

Return coeffs with all the elements negated.

SmallVector< DynamicAPInt, 8 > getDivUpperBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor, unsigned localVarIdx)

If q is defined to be equal to expr floordiv d, this equivalent to saying that q is an integer and q ...

SmallVector< DynamicAPInt, 8 > getDivLowerBound(ArrayRef< DynamicAPInt > dividend, const DynamicAPInt &divisor, unsigned localVarIdx)

SmallVector< DynamicAPInt, 8 > getComplementIneq(ArrayRef< DynamicAPInt > ineq)

Return the complement of the given inequality.

Include the generated interface declarations.

The struct CountsSnapshot stores the count of each VarKind, and also of each constraint type.

const PresburgerSpace & getSpace() const

Represents the result of a symbolic lexicographic optimization computation.

PWMAFunction lexopt

This maps assignments of symbols to the corresponding lexopt.

PresburgerSet unboundedDomain

Contains all assignments to the symbols that made the lexopt unbounded.

Eliminates variable at the specified position using Fourier-Motzkin variable elimination.