mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

sketch initial for mpz/mpq numeral creation

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-27 10:46:03 +02:00
parent 9c359713b6
commit ee80414e55
2 changed files with 60 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/api/api_numeral.cpp
View file

@ -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
};

31
src/api/z3_api.h
View file

@ -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.