From 2885a9356f35fd1b5983a0f7ea31875838685d7f Mon Sep 17 00:00:00 2001
From: Matias Barandiaran <matias.barandiaran03@gmail.com>
Date: Mon, 14 Aug 2023 11:49:35 +0200
Subject: [PATCH] Constraint Reordering: Reverse Bland Heuristic

Changes inspired by the work from:
https://link.springer.com/chapter/10.1007/978-3-319-21668-3_3
---
 src/tsolvers/lasolver/LASolver.cc | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc
index 8d3f870ce..30cca8e2a 100644
--- a/src/tsolvers/lasolver/LASolver.cc
+++ b/src/tsolvers/lasolver/LASolver.cc
@@ -913,6 +913,7 @@ TRes LASolver::cutFromProof() {
     auto isOnUpperBound = [this](LVRef var) { return simplex.hasUBound(var) and not simplex.isModelStrictlyUnderUpperBound(var); };
     // Step 1: Gather defining constraints
     std::vector<DefiningConstraint> constraints;
+    std::vector<DefiningConstraint> equalities;
     for (LVRef var : int_vars) {
         bool isOnLower = isOnLowerBound(var);
         bool isOnUpper = isOnUpperBound(var);
@@ -924,13 +925,16 @@ TRes LASolver::cutFromProof() {
         auto const & rhs = val.R();
         assert(rhs.isInteger());
         if (isOnLower and isOnUpper) {
-            constraints.insert(constraints.begin(), DefiningConstraint{term, rhs});
+            equalities.push_back(DefiningConstraint{term, rhs});
         } else {
             constraints.push_back(DefiningConstraint{term, rhs});
         }
-
-//        std::cout << logic.pp(term) << " = " << rhs << std::endl;
     }
+    for (DefiningConstraint & constraint : equalities) {
+        constraints.push_back(std::move(constraint));
+    }
+    std::reverse(constraints.begin(), constraints.end());
+
     auto getVarValue = [this](PTRef var) {
         assert(this->logic.isVar(var));
         LVRef lvar = this->laVarMapper.getVarByPTId(logic.getPterm(var).getId());