diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 60d663638..7d8c00fbe 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -459,4 +459,33 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } +#if 0 + Z3_ast Z3_API Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort* srt) { + LOG_TRY; + LOG_Z3_mk_mpz_numeral(c, sign, n, nums, srt); + RESET_ERROR_CODE(); + rational z; + + // todo fill in z + if (!z.size()) + z.neg(); + arith_util & a = mk_c(c)->autil(); + auto* a = mk_c(c)->mk_numeral_core(r, a.mk_int_sort()); + Z3_CATCH_RETURN(nullptr); + + } + + Z3_ast Z3_API Z3_mk_mpq_numeral1(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]) { + LOG_TRY; + LOG_Z3_mk_mpq_numeral(c, sign, n, nums, d, dens); + RESET_ERROR_CODE(); + rational q; + + if (!sign) + q.neg(); + + Z3_CATCH_RETURN(nullptr); + } +#endif + }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e2e7deefb..099d3d829 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3387,6 +3387,37 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty); + /** + \brief Create an integer numeral from a vector of unsigned numerals. + + \param c - context + \param sign - true if positive, false if negative + \param n - length of array of numerals + \param nums - array of numerals + \param srt - sort of numeral (int, real, bit-vector). + + future_('Z3_mk_mpz_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(SORT))) + */ + + //Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s); + + /** + \brief Create a rational numeral from a vector of unsigned numerals. + + \param c - context + \param sign - true if positive, false if negative + \param n - length of array of nominator numerals + \param nums - array of numerator numerals + \param d - length of array of denominator numerals + \param dens - array of denominator numerals + + The sort of returned numeral is Real. + + future_('Z3_mk_mpq_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT))) + */ + + // Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]); + /** \brief Create a real from a fraction.