Как получить точное представление рациональных чисел с бесконечной точностью с помощью нестандартного расширения FlatZinc?

По умолчанию mzn2fzn автоматически вычисляет результат деления с плавающей запятой в модели MiniZinc и сохраняет его как постоянное значение float в результирующем FlatZinc. модель.

Пример:

Файл test.mzn

var float: x;
constraint      1.0 / 1000000000000000000000000000000000.0 <= x;
constraint x <= 2.0 / 1000000000000000000000000000000000.0;
solve satisfy;

переведено с

mzn2fzn test.mzn

становится равным

var 1e-33..2e-33: x;
solve satisfy;

Вместо этого мы хотели бы получить*** файл FlatZinc со следующими строками:

var float: x;
var float: lb;
var float: ub;
constraint float_div(1.0, 1000000000000000000000000000000000.0, lb);
constraint float_div(2.0, 1000000000000000000000000000000000.0, ub);
solve satisfy;

где float_div() – это недавно введенное нестандартное ограничение FlatZinc.

Можно ли сгенерировать такую ​​кодировку исходной задачи, используя вариант каталога ограничений std, или эта кодировка требует более существенного изменения исходного кода инструмента mzn2fzn? В последнем случае, можем ли мы получить какое-то руководство?

***: у нас есть некоторые формулы, для которых представление с плавающей запятой конечной точности не подходит, потому что оно изменяет результат SAT на UNSAT.