Was ist eine Instanz des Optionstyps beim Parsing?

Question

Über Optionstypen, die specification von Minizinc sagt (sec 6.6.3.):

Übersicht. Optionstypen, die mit dem Konstruktor opt definiert wurden, definieren Typen, die vorhanden sein können oder nicht. Sie ähneln vielleicht Haskell-Typen, die dem Typ einen neuen Wert <> hinzufügen.

[...]

Initialisation. Eine opt-Typ-Variable muss nicht zur Instanzzeit initialisiert werden. Eine nicht initialisierte opt-type-Variable wird automatisch auf <> initialisiert.

würde Ich mag die folgende Einschränkung mit zwei opt Typen analysieren und zu verarbeiten:

predicate alternative(var opt int: s0, var int: d0, 
         array[int] of var opt int: s, 
         array[int] of var int: d); 

Aber ich bin nicht sicher, was soll ich als Werte für Argumente erwarten s0 und s beim Parsen diese Einschränkung.

Kann ich das Vorhandensein des opt Modifizierers einfach ignorieren und davon ausgehen, dass die Bedingung Signatur gleich der folgenden ist?

predicate alternative(var int: s0, var int: d0, 
         array[int] of var int: s, 
         array[int] of var int: d); 

Wenn nicht, wie soll ich damit umgehen?

Answer 1

In MiniZinc Variablenvariablentypen werden als Variablen behandelt, die möglicherweise nicht vorhanden sind. Innerhalb des Compilers werden diese Variablen transformiert. Diese Variablen werden interpretiert und so umgeschrieben, dass die FlatZinc-Ausgabe nur tatsächliche Variablen enthält. Normalerweise bedeutet dies, dass eine boolesche Variable für jede Variable hinzugefügt wird, die nur dann wahr ist, wenn die Variable "existiert".

Für die Bibliotheksschreiber gibt es die Möglichkeit, sie so umzuschreiben, dass Ihr Solver am besten damit umgehen kann. In der Standardbibliothek wird alternative definiert als:

predicate alternative(var opt int: s0, var int: d0, 
        array[int] of var opt int: s, 
        array[int] of var int: d) = 
      assert(index_set(s) = index_set(d), 
       "alternative: index sets of third and fourth argument must be identical", 
      sum(i in index_set(s))(bool2int(occurs(s[i]))) <= 1 /\ 
      span(s0,d0,s,d) 
    ); 

bemerken, dass die intrinsischen occurs verwendet wird, um zu testen, ob eine Variable existiert. Weitere Intrinsics für Variablentypen finden Sie in der MiniZinc-Bibliothek: http://www.minizinc.org/doc-lib/doc-optiontypes.html. Bei Bedarf können Sie auch einen let-expression verwenden, um eine zusätzliche Variable zu erstellen und dann das Prädikat einem intrinsischen Prädikat des Lösers zuzuordnen.

Auch wenn es keine bessere Zerlegung des optionalen Typprädikats für Ihren Solver gibt, kann es dennoch sinnvoll sein, das Prädikat ohne Optionstypen zu implementieren. Aufgrund der Überlastung von MiniZinc wird diese Implementierung immer dann verwendet, wenn das Prädikat mit Arrays von Nicht-Option-Variablentypen aufgerufen wird. (Beachten Sie jedoch, dass das Prädikat alternative speziell für "optionale Aufgaben" gedacht ist und wahrscheinlich nicht so genannt wird).