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);
  final d = c._createAST(arg2);
  switch (kind) {
    case TernaryOpKind.ite:
      return c._z3.mk_ite(a, b, d);
    case TernaryOpKind.store:
      return c._z3.mk_store(a, b, d);
    case TernaryOpKind.seqExtract:
      return c._z3.mk_seq_extract(a, b, d);
    case TernaryOpKind.seqReplace:
      return c._z3.mk_seq_replace(a, b, d);
    case TernaryOpKind.seqIndex:
      return c._z3.mk_seq_index(a, b, d);
    case TernaryOpKind.fpaFp:
      final sort = c.getSort(arg0);
      assert(sort is BitVecSort && sort.size == 1);
      return c._z3.mk_fpa_fp(a, b, d);
    case TernaryOpKind.fpaAdd:
      return c._z3.mk_fpa_add(a, b, d);
    case TernaryOpKind.fpaSub:
      return c._z3.mk_fpa_sub(a, b, d);
    case TernaryOpKind.fpaMul:
      return c._z3.mk_fpa_mul(a, b, d);
    case TernaryOpKind.fpaDiv:
      return c._z3.mk_fpa_div(a, b, d);
  }
}