From c6a967f23a254ec85f50a83266826f74c7f77ef5 Mon Sep 17 00:00:00 2001
From: "Jip J. Dekker" <jip@dekker.one>
Date: Tue, 13 Jul 2021 15:23:55 +1000
Subject: [PATCH] Squashed 'software/mza/' changes from 15b5b1ca03..b74e0a6989

b74e0a6989 Use correct bounds when only infinite on one side
4b12442928 Use Val comparison for infinity check
5a4119666a Add untrailing for constraint removal
b44ed554c6 FIXME: do not clear global registers. This does not work in the incremental case
4fce29b144 Ensure trailing of aliases happens after actual aliasing operations

git-subtree-dir: software/mza
git-subtree-split: b74e0a698981985cdf4979c6e533ded5d2adc349
---
 lib/interpreter.cpp                      | 2 +-
 lib/interpreter/variable.cpp             | 2 +-
 lib/solver.cpp                           | 2 +-
 solvers/gecode/gecode_constraints.cpp    | 4 +++-
 solvers/gecode/gecode_solverinstance.cpp | 2 +-
 5 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/lib/interpreter.cpp b/lib/interpreter.cpp
index 442e4c4..dbe9945 100644
--- a/lib/interpreter.cpp
+++ b/lib/interpreter.cpp
@@ -1555,7 +1555,7 @@ void Trail::untrail(MiniZinc::Interpreter* interpreter) {
       assert(var->definitions().back() == con);
       var->_definitions.pop_back();
     } else {
-      assert(false);
+      var->_definitions.push_back(con);
     }
     def_trail.pop_back();
   }
diff --git a/lib/interpreter/variable.cpp b/lib/interpreter/variable.cpp
index 63c5e63..639fecf 100644
--- a/lib/interpreter/variable.cpp
+++ b/lib/interpreter/variable.cpp
@@ -346,10 +346,10 @@ void Variable::alias(Interpreter* interpreter, Val v) {
   _subscriptions.clear();
 
   // Set Alias
-  interpreter->trail.trail_alias(interpreter, this);
   _aliased = true;
   _domain = v;
   v.addRef(interpreter);
+  interpreter->trail.trail_alias(interpreter, this);
 }
 
 void Variable::unalias(Interpreter* interpreter, Val dom) {
diff --git a/lib/solver.cpp b/lib/solver.cpp
index a3218ee..159c5ad 100644
--- a/lib/solver.cpp
+++ b/lib/solver.cpp
@@ -817,7 +817,7 @@ void MznSolver::flatten(const std::string& filename, const std::string& modelNam
   }
   flatten_time = tm01.s();
   // FIXME: Global registers should not be removed, merely hidden
-  interpreter->clear_globals();
+  // interpreter->clear_globals();
   if (verbose) {
     std::cerr << "Status: " << Interpreter::status_to_string[interpreter->status()] << std::endl;
     if (interpreter->status() == Interpreter::ROGER) {
diff --git a/solvers/gecode/gecode_constraints.cpp b/solvers/gecode/gecode_constraints.cpp
index b7aaca3..c48a2b3 100644
--- a/solvers/gecode/gecode_constraints.cpp
+++ b/solvers/gecode/gecode_constraints.cpp
@@ -38,7 +38,9 @@ void p_mk_intvar(SolverInstanceBase& s, const Variable* var, bool isOutput) {
       gi._current_space->iv_defined.push_back(!var->definitions().empty());
     }
   } else {
-    IntVar intVar(*gi._current_space, Gecode::Int::Limits::min, Gecode::Int::Limits::max);
+    IntVar intVar(*gi._current_space,
+                  var->lb().isFinite() ? var->lb().toInt() : Gecode::Int::Limits::min,
+                  var->ub().isFinite() ? var->ub().toInt() : Gecode::Int::Limits::max);
     gi._current_space->iv.push_back(intVar);
     gi.insertVar(var, GecodeVariable(GecodeVariable::INT_TYPE, gi._current_space->iv.size() - 1));
     std::cerr << "% GecodeSolverInstance::processFlatZinc: Warning: Unbounded variable "
diff --git a/solvers/gecode/gecode_solverinstance.cpp b/solvers/gecode/gecode_solverinstance.cpp
index 61c6ff1..ce9150c 100644
--- a/solvers/gecode/gecode_solverinstance.cpp
+++ b/solvers/gecode/gecode_solverinstance.cpp
@@ -1152,7 +1152,7 @@ bool GecodeSolverInstance::isBoolArray(const Val& arr, int& singleInt) {
     if (val.isInt() && val >= 0 && val <= 1) {
       continue;
     } else if (val.isVar()) {
-      if (val.lb().toInt() >= 0 && val.ub().toInt() <= 1) {
+      if (val.lb() >= Val(int(0)) && val.ub() <= Val(int(1))) {
         continue;
       }
       return false;