mk_ite method

Z3_ast mk_ite(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3,)

\brief Create an AST node representing an if-then-else: \ccode{ite(t1, t2, t3)}.

The node \c t1 must have Boolean sort, \c t2 and \c t3 must have the same sort. The sort of the new node is equal to the sort of \c t2 and \c t3.

def_API('Z3_mk_ite', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))

Implementation

Z3_ast mk_ite(
  Z3_context c,
  Z3_ast t1,
  Z3_ast t2,
  Z3_ast t3,
) {
  return _mk_ite(
    c,
    t1,
    t2,
    t3,
  );
}