build method

@override Z3_ast build(Context c)

Implementation

@override
Z3_ast build(Context c) {
  final a = c._createAST(arg0);
  final b = c._createAST(arg1);
  switch (kind) {
    case BinaryOpKind.eq:
      return c._z3.mk_eq(a, b);
    case BinaryOpKind.implies:
      return c._z3.mk_implies(a, b);
    case BinaryOpKind.xor:
      return c._z3.mk_xor(a, b);
    case BinaryOpKind.div:
      return c._z3.mk_div(a, b);
    case BinaryOpKind.mod:
      return c._z3.mk_mod(a, b);
    case BinaryOpKind.rem:
      return c._z3.mk_rem(a, b);
    case BinaryOpKind.pow:
      return c._z3.mk_power(a, b);
    case BinaryOpKind.lt:
      return c._z3.mk_lt(a, b);
    case BinaryOpKind.le:
      return c._z3.mk_le(a, b);
    case BinaryOpKind.gt:
      return c._z3.mk_gt(a, b);
    case BinaryOpKind.ge:
      return c._z3.mk_ge(a, b);
    case BinaryOpKind.bvAnd:
      return c._z3.mk_bvand(a, b);
    case BinaryOpKind.bvOr:
      return c._z3.mk_bvor(a, b);
    case BinaryOpKind.bvXor:
      return c._z3.mk_bvxor(a, b);
    case BinaryOpKind.bvNand:
      return c._z3.mk_bvnand(a, b);
    case BinaryOpKind.bvNor:
      return c._z3.mk_bvnor(a, b);
    case BinaryOpKind.bvXnor:
      return c._z3.mk_bvxnor(a, b);
    case BinaryOpKind.bvAdd:
      return c._z3.mk_bvadd(a, b);
    case BinaryOpKind.bvSub:
      return c._z3.mk_bvsub(a, b);
    case BinaryOpKind.bvMul:
      return c._z3.mk_bvmul(a, b);
    case BinaryOpKind.bvUdiv:
      return c._z3.mk_bvudiv(a, b);
    case BinaryOpKind.bvSdiv:
      return c._z3.mk_bvsdiv(a, b);
    case BinaryOpKind.bvUrem:
      return c._z3.mk_bvurem(a, b);
    case BinaryOpKind.bvSrem:
      return c._z3.mk_bvsrem(a, b);
    case BinaryOpKind.bvSmod:
      return c._z3.mk_bvsmod(a, b);
    case BinaryOpKind.bvUlt:
      return c._z3.mk_bvult(a, b);
    case BinaryOpKind.bvSlt:
      return c._z3.mk_bvslt(a, b);
    case BinaryOpKind.bvUle:
      return c._z3.mk_bvule(a, b);
    case BinaryOpKind.bvSle:
      return c._z3.mk_bvsle(a, b);
    case BinaryOpKind.bvUge:
      return c._z3.mk_bvuge(a, b);
    case BinaryOpKind.bvSge:
      return c._z3.mk_bvsge(a, b);
    case BinaryOpKind.bvUgt:
      return c._z3.mk_bvugt(a, b);
    case BinaryOpKind.bvSgt:
      return c._z3.mk_bvsgt(a, b);
    case BinaryOpKind.bvConcat:
      return c._z3.mk_concat(a, b);
    case BinaryOpKind.bvShl:
      return c._z3.mk_bvshl(a, b);
    case BinaryOpKind.bvLshr:
      return c._z3.mk_bvlshr(a, b);
    case BinaryOpKind.bvAshr:
      return c._z3.mk_bvashr(a, b);
    case BinaryOpKind.bvRotl:
      return c._z3.mk_ext_rotate_left(a, b);
    case BinaryOpKind.bvRotr:
      return c._z3.mk_ext_rotate_right(a, b);
    case BinaryOpKind.bvSMulNoUnderflow:
      return c._z3.mk_bvmul_no_underflow(a, b);
    case BinaryOpKind.bvUMulNoOverflow:
      return c._z3.mk_bvmul_no_overflow(a, b, false);
    case BinaryOpKind.bvSMulNoOverflow:
      return c._z3.mk_bvmul_no_overflow(a, b, true);
    case BinaryOpKind.setDifference:
      return c._z3.mk_set_difference(a, b);
    case BinaryOpKind.setSubset:
      return c._z3.mk_set_subset(a, b);
    case BinaryOpKind.seqPrefix:
      return c._z3.mk_seq_prefix(a, b);
    case BinaryOpKind.seqSuffix:
      return c._z3.mk_seq_suffix(a, b);
    case BinaryOpKind.seqContains:
      return c._z3.mk_seq_contains(a, b);
    case BinaryOpKind.strLt:
      return c._z3.mk_str_lt(a, b);
    case BinaryOpKind.strLe:
      return c._z3.mk_str_le(a, b);
    case BinaryOpKind.seqAt:
      return c._z3.mk_seq_at(a, b);
    case BinaryOpKind.seqNth:
      return c._z3.mk_seq_nth(a, b);
    case BinaryOpKind.seqLastIndex:
      return c._z3.mk_seq_last_index(a, b);
    case BinaryOpKind.seqInRe:
      return c._z3.mk_seq_in_re(a, b);
    case BinaryOpKind.reRange:
      return c._z3.mk_re_range(a, b);
    case BinaryOpKind.reDiff:
      return c._z3.mk_re_diff(a, b);
    case BinaryOpKind.charLe:
      return c._z3.mk_char_le(a, b);
    case BinaryOpKind.fpaSqrt:
      return c._z3.mk_fpa_sqrt(a, b);
    case BinaryOpKind.fpaRem:
      return c._z3.mk_fpa_rem(a, b);
    case BinaryOpKind.fpaMin:
      return c._z3.mk_fpa_min(a, b);
    case BinaryOpKind.fpaMax:
      return c._z3.mk_fpa_max(a, b);
    case BinaryOpKind.fpaLeq:
      return c._z3.mk_fpa_leq(a, b);
    case BinaryOpKind.fpaLt:
      return c._z3.mk_fpa_lt(a, b);
    case BinaryOpKind.fpaGeq:
      return c._z3.mk_fpa_geq(a, b);
    case BinaryOpKind.fpaGt:
      return c._z3.mk_fpa_gt(a, b);
    case BinaryOpKind.fpaEq:
      return c._z3.mk_fpa_eq(a, b);
  }
}