mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-19 21:02:15 -07:00
commit 7cc6d84e6f
53 changed files with 112 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

36
src/api/api_fpa.cpp
View file

@ -913,7 +913,7 @@ extern "C" {
CHECK_VALID_AST(t, 0);
if (sgn == nullptr) {
SET_ERROR_CODE(Z3_INVALID_ARG, "sign cannot be a nullpointer");
return 0;
return false;
}
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@ -922,13 +922,13 @@ extern "C" {
expr * e = to_expr(t);
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
return 0;
return false;
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(to_expr(t), val);
if (!r || mpfm.is_nan(val)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
return 0;
return false;
}
*sgn = mpfm.sgn(val);
return r;
@ -1043,7 +1043,7 @@ extern "C" {
CHECK_VALID_AST(t, 0);
if (n == nullptr) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid nullptr argument");
return 0;
return false;
}
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@ -1055,7 +1055,7 @@ extern "C" {
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
*n = 0;
return 0;
return false;
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
@ -1065,10 +1065,10 @@ extern "C" {
!mpzm.is_uint64(z)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
*n = 0;
return 0;
return false;
}
*n = mpzm.get_uint64(z);
return 1;
return true;
Z3_CATCH_RETURN(0);
}
@ -1121,7 +1121,7 @@ extern "C" {
CHECK_VALID_AST(t, 0);
if (n == nullptr) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid null argument");
return 0;
return false;
}
ast_manager & m = mk_c(c)->m();
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
@ -1132,14 +1132,14 @@ extern "C" {
if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
*n = 0;
return 0;
return false;
}
scoped_mpf val(mpfm);
bool r = plugin->is_numeral(e, val);
if (!r || !(mpfm.is_normal(val) || mpfm.is_denormal(val) || mpfm.is_zero(val) || mpfm.is_inf(val))) {
SET_ERROR_CODE(Z3_INVALID_ARG, "invalid expression argument, expecting a valid fp, not a NaN");
*n = 0;
return 0;
return false;
}
unsigned ebits = val.get().get_ebits();
if (biased) {
@ -1153,7 +1153,7 @@ extern "C" {
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.exp(val);
}
return 1;
return true;
Z3_CATCH_RETURN(0);
}
@ -1240,7 +1240,7 @@ extern "C" {
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
return false;
}
return fu.is_nan(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
@ -1254,7 +1254,7 @@ extern "C" {
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
return false;
}
return fu.is_inf(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
@ -1268,7 +1268,7 @@ extern "C" {
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
return false;
}
return fu.is_zero(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
@ -1282,7 +1282,7 @@ extern "C" {
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
return false;
}
return fu.is_normal(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
@ -1296,7 +1296,7 @@ extern "C" {
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
return false;
}
return fu.is_subnormal(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
@ -1310,7 +1310,7 @@ extern "C" {
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
return false;
}
return fu.is_positive(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
@ -1324,7 +1324,7 @@ extern "C" {
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return 0;
return false;
}
return fu.is_negative(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);

4
src/api/api_quant.cpp
View file

@ -132,7 +132,7 @@ extern "C" {
unsigned num_decls, Z3_sort const types[],
Z3_symbol const decl_names[],
Z3_ast body) {
return Z3_mk_quantifier(c, 1, weight, num_patterns, patterns, num_decls, types, decl_names, body);
return Z3_mk_quantifier(c, true, weight, num_patterns, patterns, num_decls, types, decl_names, body);
}
Z3_ast Z3_API Z3_mk_exists(Z3_context c,
@ -141,7 +141,7 @@ extern "C" {
unsigned num_decls, Z3_sort const types[],
Z3_symbol const decl_names[],
Z3_ast body) {
return Z3_mk_quantifier(c, 0, weight, num_patterns, patterns, num_decls, types, decl_names, body);
return Z3_mk_quantifier(c, false, weight, num_patterns, patterns, num_decls, types, decl_names, body);
}
Z3_ast Z3_API Z3_mk_lambda(Z3_context c,

4
src/api/c++/z3++.h
View file

@ -277,7 +277,7 @@ namespace z3 {
*/
sort fpa_rounding_mode();
/**
\breif Sets RoundingMode of FloatingPoints.
\brief Sets RoundingMode of FloatingPoints.
*/
void set_rounding_mode(rounding_mode rm);
/**
@ -291,7 +291,7 @@ namespace z3 {
\brief Return a tuple constructor.
\c name is the name of the returned constructor,
\c n are the number of arguments, \c names and \c sorts are their projected sorts.
\c projs is an output paramter. It contains the set of projection functions.
\c projs is an output parameter. It contains the set of projection functions.
*/
func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);

6
src/api/python/z3/z3.py
View file

@ -8327,7 +8327,7 @@ def prove(claim, **keywords):
print(s.model())
def _solve_html(*args, **keywords):
"""Version of funcion `solve` used in RiSE4Fun."""
"""Version of function `solve` used in RiSE4Fun."""
s = Solver()
s.set(**keywords)
s.add(*args)
@ -8349,7 +8349,7 @@ def _solve_html(*args, **keywords):
print(s.model())
def _solve_using_html(s, *args, **keywords):
"""Version of funcion `solve_using` used in RiSE4Fun."""
"""Version of function `solve_using` used in RiSE4Fun."""
if __debug__:
_z3_assert(isinstance(s, Solver), "Solver object expected")
s.set(**keywords)
@ -8372,7 +8372,7 @@ def _solve_using_html(s, *args, **keywords):
print(s.model())
def _prove_html(claim, **keywords):
"""Version of funcion `prove` used in RiSE4Fun."""
"""Version of function `prove` used in RiSE4Fun."""
if __debug__:
_z3_assert(is_bool(claim), "Z3 Boolean expression expected")
s = Solver()

2
src/api/z3_optimization.h
View file

@ -146,7 +146,7 @@ extern "C" {
Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o);
/**
\brief Retrieve the unsat core for the last #Z3_optimize_chec
\brief Retrieve the unsat core for the last #Z3_optimize_check
The unsat core is a subset of the assumptions \c a.
def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE)))