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

Question

По умолчанию 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.

Answer 1

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

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