Каковы эти ограничения `float_div` и` float_times` в файле FlatZinc? - PullRequest
Новая
       17

Каковы эти ограничения `float_div` и` float_times` в файле FlatZinc?

0 голосов
/ 21 декабря 2018

Я только что попытался запустить mzn2fzn для следующего файла MiniZinc : 

var float: x1;
var float: y1;
var float: x2;
var float: y2;
constraint (x1 / y1) = 6.0;
constraint x2 * y2 <= 5.0;
solve satisfy;

Это итоговый файл FlatZinc : 

var -1.7976931348623157e+308..5.0: FLOAT____00001 :: is_defined_var :: var_is_introduced;
var float: x1;
var float: x2;
var float: y1;
var float: y2;
constraint float_div(x1, y1, 6.0);
constraint float_times(x2, y2, FLOAT____00001) :: defines_var(FLOAT____00001);
solve satisfy;

Версия mzn2fzn выглядит следующим образом: 

~$ mzn2fzn --version
G12 MiniZinc to FlatZinc converter, version 1.6.0
Copyright (C) 2006-2012 The University of Melbourne and NICTA

У меня есть следующие вопросы:

  • что такое ограничение float_div, которое не кажетсябыть упомянутым в FlatZinc 1.6 Standard ?
  • Что такое ограничение float_times, которое, по-видимому, не упоминается в FlatZinc 1.6 Standard ?

Поддерживает ли их какой-либо решатель FlatZinc на самом деле?

NB Я действительно нашел след этих функций в документах для FlatZinc 2.2.0 , однако, я не понимаю, почему они генерируются версией 1.6 mzn2fzn, когда в документации не упоминается ни один из них.

1 Ответ

0 голосов
/ 21 декабря 2018

Кажется, что в документации FlatZinc 1.6 есть упущение, что ограничения float_div и float_times не задокументированы.Эти ограничения являются необходимыми частями встроенных модулей FlatZinc, которые должны быть понятны специалистам с поддержкой переменных с плавающей запятой.Их нельзя переписать в другие ограничения, которые есть среди встроенных функций FlatZinc, и поэтому компилятор будет их использовать.Я хотел бы отметить, что int_div и int_times задокументированы в документации старой версии FlatZinc, и значение ограничений можно экстраполировать из этих ограничений.(У меня также сложилось впечатление, что их значение не изменилось при преобразовании в FlatZinc 2.2.0)

Gecode, CP-решатель, поставляемый с MiniZinc, поддерживает эти ограничения.

...