mk_numeral method

Z3_ast mk_numeral(
  1. Z3_context c,
  2. Z3_string numeral,
  3. Z3_sort ty
)

@name Numerals / /**@{/ /** \brief Create a numeral of a given sort.

\param c logical context. \param numeral A string representing the numeral value in decimal notation. The string may be of the form [num]*[.[num]*][E[+|-][num]+]. If the given sort is a real, then the numeral can be a rational, that is, a string of the form [num]* / [num]* . \param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.

\sa Z3_mk_int \sa Z3_mk_unsigned_int

def_API('Z3_mk_numeral', AST, (_in(CONTEXT), _in(STRING), _in(SORT)))

Implementation

Z3_ast mk_numeral(
  Z3_context c,
  Z3_string numeral,
  Z3_sort ty,
) {
  return _mk_numeral(
    c,
    numeral,
    ty,
  );
}