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

Question

По умолчанию mzn2fzn автоматически вычисляет результат деления с плавающей запятой в модели MiniZinc и сохраняет его как постоянное значение с плавающей запятой в результирующей модели 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,

Answer 1

В настоящее время нет способа генерирования FlatZinc с бесконечной точностью. Хотя эта идея обсуждалась несколько раз, для ее переписывания или добавления большей части MiniZinc потребуется библиотека, которая может предоставить эти бесконечно точные типы. Такие библиотеки, как Boost interval библиотека, похоже, не хватает опций и в настоящее время не компилируется для всех машинных целей, на которых распространяется MiniZinc. Кажется, существуют разные интересные случаи для бесконечно точных типов, но в рамках реализации компилятора MiniZinc мы все еще ищем достойный способ их реализации.

Хотя бесконечной точности нет на столе. Компилятор MiniZinc намерен быть правильным в соответствии со стандартами с плавающей запятой. Не стесняйтесь сообщать о любых проблемах, которые могут возникнуть в MiniZinc Issue Tracker.