operator [] method

Expr operator [](Object index)

Indexes an array or tuple expression using the given index.

If the array has multiple domains, index should be a list of expressions.

Note that this operator does not index an array directly, rather it returns an expression that represents the indexing operation. Pass the result to Model.eval to retrieve a concrete value.

Implementation

Expr operator [](Object index) {
  final sort = getSort(this);
  if (sort is ArraySort) {
    if (index is List<Object>) {
      return selectN(this, index.map($));
    } else {
      return select(this, $(index));
    }
  } else if (sort is DatatypeSort) {
    final info = getDatatypeInfo(sort);
    if (info.constructors.length != 1) {
      throw ArgumentError.value(
        this,
        'this',
        'datatype sort has more than one constructor',
      );
    }
    final accessors = info.constructors.single.accessors;
    if (index is Sym) {
      return app(accessors.singleWhere((e) => e.name == index), this);
    } else if (index is int) {
      return app(accessors[index], this);
    } else if (index is String) {
      return app(accessors.singleWhere((e) => e.name == Sym(index)), this);
    } else {
      throw ArgumentError.value(
        index,
        'index',
        'not a valid datatype accessor',
      );
    }
  } else {
    throw ArgumentError.value(this, 'this', 'not an array');
  }
}