build method

@override Z3_ast build(Context c)

Implementation

@override
Z3_ast build(Context c) {
  final a = c._createAST(arg);
  switch (kind) {
    case UnaryOpKind.not:
      return c._z3.mk_not(a);
    case UnaryOpKind.unaryMinus:
      return c._z3.mk_unary_minus(a);
    case UnaryOpKind.intToReal:
      return c._z3.mk_int2real(a);
    case UnaryOpKind.realToInt:
      return c._z3.mk_real2int(a);
    case UnaryOpKind.isInt:
      return c._z3.mk_is_int(a);
    case UnaryOpKind.bvNot:
      return c._z3.mk_bvnot(a);
    case UnaryOpKind.bvRedAnd:
      return c._z3.mk_bvredand(a);
    case UnaryOpKind.bvRedOr:
      return c._z3.mk_bvredor(a);
    case UnaryOpKind.bvNeg:
      return c._z3.mk_bvneg(a);
    case UnaryOpKind.arrayDefault:
      return c._z3.mk_array_default(a);
    case UnaryOpKind.setComplement:
      return c._z3.mk_set_complement(a);
    case UnaryOpKind.seqUnit:
      return c._z3.mk_seq_unit(a);
    case UnaryOpKind.seqLength:
      return c._z3.mk_seq_length(a);
    case UnaryOpKind.strToInt:
      return c._z3.mk_str_to_int(a);
    case UnaryOpKind.intToStr:
      return c._z3.mk_int_to_str(a);
    case UnaryOpKind.strToCode:
      return c._z3.mk_string_to_code(a);
    case UnaryOpKind.codeToStr:
      return c._z3.mk_string_from_code(a);
    case UnaryOpKind.ubvToStr:
      return c._z3.mk_ubv_to_str(a);
    case UnaryOpKind.sbvToStr:
      return c._z3.mk_sbv_to_str(a);
    case UnaryOpKind.seqToRe:
      return c._z3.mk_seq_to_re(a);
    case UnaryOpKind.rePlus:
      return c._z3.mk_re_plus(a);
    case UnaryOpKind.reStar:
      return c._z3.mk_re_star(a);
    case UnaryOpKind.reOption:
      return c._z3.mk_re_option(a);
    case UnaryOpKind.reComplement:
      return c._z3.mk_re_complement(a);
    case UnaryOpKind.charToInt:
      return c._z3.mk_char_to_int(a);
    case UnaryOpKind.charToBv:
      return c._z3.mk_char_to_bv(a);
    case UnaryOpKind.bvToChar:
      return c._z3.mk_char_from_bv(a);
    case UnaryOpKind.charIsDigit:
      return c._z3.mk_char_is_digit(a);
    case UnaryOpKind.fpaAbs:
      return c._z3.mk_fpa_abs(a);
    case UnaryOpKind.fpaNeg:
      return c._z3.mk_fpa_neg(a);
    case UnaryOpKind.fpaIsNormal:
      return c._z3.mk_fpa_is_normal(a);
    case UnaryOpKind.fpaIsSubnormal:
      return c._z3.mk_fpa_is_subnormal(a);
    case UnaryOpKind.fpaIsZero:
      return c._z3.mk_fpa_is_zero(a);
    case UnaryOpKind.fpaIsInfinite:
      return c._z3.mk_fpa_is_infinite(a);
    case UnaryOpKind.fpaIsNaN:
      return c._z3.mk_fpa_is_nan(a);
    case UnaryOpKind.fpaIsNegative:
      return c._z3.mk_fpa_is_negative(a);
    case UnaryOpKind.fpaIsPositive:
      return c._z3.mk_fpa_is_positive(a);
    case UnaryOpKind.fpaToReal:
      return c._z3.mk_fpa_to_real(a);
    case UnaryOpKind.fpaToIeeeBv:
      return c._z3.mk_fpa_to_ieee_bv(a);
  }
}