Instantiation in Minizinc

Viewed 47

I am reading through "A Minizinc Tutorial" by Kim Marriott and it says that

the combination of variable instantiation and type is called type-inst. As you start to use Minizinc, you will undoubtedly see examples of type-inst errors.

What exactly are type-inst errors?

1 Answers

I believe the terminology is not often used in the MiniZinc literature these days, but for every value in MiniZinc the compiler keeps track of two things: it's type (int, bool, float, etc.) and if it is a decision variable (not known at solve time) or a problem parameter (must be known when rewriting the model for the solver). Together these two things are called the Type Instantiation or type-inst.

A type-inst error is an error given by the type checker of the compiler. These error can occur in many places, such as when in a declaration the declared type instantiation doesn't match it's right hand side, or when two side of an if-then-else have a different type-instantiation, or when the arguments of a call do not match the declared type-instantiation of the function-declaration.

The mismatch that causes these errors can come from either side of the type-inst: either the types are incompatible (e.g. used float instead of bool), or you used a decision variable where only a problem parameter was allowed. These issues are usually caused by mistakes in the model and are usually resolved easily by changing the value used or using different language constructs.

Note that MiniZinc does allow sub-typing: You are allowed to use bool instead of int and it is converted to a 0/1 value. Similarly you can use a integer value instead of a float, and you can use a parameter in place of a variable.

The newest version of the MiniZinc Tutorial can be found with its documentation: https://www.minizinc.org/doc-latest/en/part_2_tutorial.html

Related