MiniZinc实现点到线段整数距离函数报int out of range错误求解

• 手动设置的变量定义域与实际可能取值范围不匹配，触发整数溢出：
  你为dot变量设置的定义域是-200..200，但实际(x-x1)*(x2-x1)单项的取值范围就能到-10000..10000，两项相加后dot的实际范围是-20000..20000，远超出你设置的范围。MiniZinc编译时会计算所有变量的可能取值组合，超出手动设置域的部分会触发整数运算溢出，因此生成了-8004400200000这类超出32位整数范围的非法值。
• 变量定义域与赋值逻辑冲突，导致FlatZinc生成语法错误：
  你为param变量设置的定义域是0..2000，但分支逻辑中当len==0时会给param赋值-1，-1不在设置的定义域范围内。MiniZinc编译生成FlatZinc格式时会生成非法的范围表达式，因此抛出unexpected FZ_DOTDOT的语法错误。
• 额外逻辑问题：pointLine函数中的插值公式写错，你用了x1-x2的差值，实际应该是x2-x1，否则会出现坐标反向计算的问题，也可能导致取值超出定义域触发溢出。

1. 修正所有变量的定义域，和实际取值范围匹配：
   • dot定义域改为-20000..20000
   • len是平方和，不可能为负，定义域改为0..20000
   • param可能取-1，定义域改为-1..2000
   • dot10是dot乘10的结果，定义域改为-200000..200000
2. 修正pointLine函数的插值公式
3. 补充len==0的分支处理，避免出现除零和非法取值

修复后可运行代码 #

var 0..100: u;
var 0..100: v;
var 0..100: w;
var 0..100: x;
var 0..100: y;
var 0..100: z;

var 0..20000: a = distancePointLine(u, v, w, x, y, z);

function var 0..20000: distancePointLine(var 0..100: x, var 0..100: y, var 0..100: x1, var 0..100: y1, var 0..100: x2, var 0..100: y2) =
  let {
  var -20000..20000: dot = (x-x1) * (x2-x1) + (y-y1) * (y2-y1);
  var -200000..200000: dot10 = dot * 10;
  var 0..20000: len = (x2-x1) * (x2-x1) + (y2-y1) * (y2-y1);
  var -1..2000: param = if len == 0 then -1 else dot div len endif;
  var 0..10: onLine = if param != 0 \/ len == 0 then 0 else dot10 div len endif;
  var 0..100: xLine = if param < 0 \/ len == 0 then x1 elseif param >= 1 then x2 else pointLine(x1,x2,onLine) endif;
  var 0..100: yLine = if param < 0 \/ len == 0 then y1 elseif param >= 1 then y2 else pointLine(y1,y2,onLine) endif;
  var 0..20000: distance = (x-xLine) * (x - xLine) + (y-yLine) * (y-yLine);
  } in distance;
  
function var 0..100: pointLine(var 0..100: x1, var 0..100: x2, var 0..10: segment) = 
  let {
    var 0..100: point = x1 + segment * (x2 - x1) div 10;
  } in point;
  
solve maximize a;

output [
         "Res: \(a) ",
         ];

内容的提问来源于stack exchange，提问作者Wouter Morssink