Skip to content

Commit

Permalink
lint
Browse files Browse the repository at this point in the history
  • Loading branch information
hzfan committed Jan 27, 2021
1 parent b1f799d commit 2acd72b
Showing 1 changed file with 17 additions and 20 deletions.
37 changes: 17 additions & 20 deletions src/arith/solve_linear_inequality.cc
Original file line number Diff line number Diff line change
Expand Up @@ -94,11 +94,10 @@ struct ExprLess {
}
};

void DebugPrint(
const std::vector<PrimExpr>& current_ineq_set,
const std::vector<PrimExpr>& next_ineq_set,
const std::vector<PrimExpr>& rest, const std::vector<std::pair<int64_t, PrimExpr>>& coef_pos,
const std::vector<std::pair<int64_t, PrimExpr>>& coef_neg) {
void DebugPrint(const std::vector<PrimExpr>& current_ineq_set,
const std::vector<PrimExpr>& next_ineq_set, const std::vector<PrimExpr>& rest,
const std::vector<std::pair<int64_t, PrimExpr>>& coef_pos,
const std::vector<std::pair<int64_t, PrimExpr>>& coef_neg) {
std::cout << "Current ineq set:\n[";
for (auto& ineq : current_ineq_set) {
std::cout << ineq << ", ";
Expand Down Expand Up @@ -148,10 +147,12 @@ class NormalizeComparisons : public ExprMutator {
arith::Analyzer analyzer_;
};

void AddInequality(std::vector<PrimExpr>* inequality_set,
const PrimExpr& new_ineq, Analyzer* analyzer) {
if (analyzer->CanProve(new_ineq) || std::find_if(inequality_set->begin(), inequality_set->end(),
[&](const PrimExpr& e) { return StructuralEqual()(e, new_ineq); }) != inequality_set->end()) {
void AddInequality(std::vector<PrimExpr>* inequality_set, const PrimExpr& new_ineq,
Analyzer* analyzer) {
if (analyzer->CanProve(new_ineq) ||
std::find_if(inequality_set->begin(), inequality_set->end(), [&](const PrimExpr& e) {
return StructuralEqual()(e, new_ineq);
}) != inequality_set->end()) {
// redundant: follows from the vranges
// or has already been added
return;
Expand All @@ -172,12 +173,10 @@ void AddInequality(std::vector<PrimExpr>* inequality_set,
inequality_set->push_back(new_ineq);
}

void ClassifyByPolarity(
const Var& var,
const std::vector<PrimExpr>& current_ineq_set,
std::vector<PrimExpr>* next_ineq_set,
std::vector<PrimExpr>* rest, std::vector<std::pair<int64_t, PrimExpr>>* coef_pos,
std::vector<std::pair<int64_t, PrimExpr>>* coef_neg, Analyzer* analyzer) {
void ClassifyByPolarity(const Var& var, const std::vector<PrimExpr>& current_ineq_set,
std::vector<PrimExpr>* next_ineq_set, std::vector<PrimExpr>* rest,
std::vector<std::pair<int64_t, PrimExpr>>* coef_pos,
std::vector<std::pair<int64_t, PrimExpr>>* coef_neg, Analyzer* analyzer) {
// Take formulas from current_ineq_set and classify them according to polarity wrt var
// and store to coef_pos and coef_neg respectively.
for (const PrimExpr& ineq : current_ineq_set) {
Expand Down Expand Up @@ -219,14 +218,12 @@ void ClassifyByPolarity(
}
}

void MoveEquality(std::vector<PrimExpr>* upper_bounds,
std::vector<PrimExpr>* lower_bounds,
void MoveEquality(std::vector<PrimExpr>* upper_bounds, std::vector<PrimExpr>* lower_bounds,
std::vector<PrimExpr>* equalities) {
// those exist in both upper & lower bounds will be moved to equalities
for (auto ub = upper_bounds->begin(); ub != upper_bounds->end();) {
auto lb = std::find_if(lower_bounds->begin(), lower_bounds->end(), [&](const PrimExpr& e) {
return StructuralEqual()(e, *ub);
});
auto lb = std::find_if(lower_bounds->begin(), lower_bounds->end(),
[&](const PrimExpr& e) { return StructuralEqual()(e, *ub); });
if (lb != lower_bounds->end()) {
equalities->push_back(*lb);
lower_bounds->erase(lb);
Expand Down

0 comments on commit 2acd72b

Please sign in to comment.