mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

Merge pull request #2021 from waywardmonkeys/api-bool-reduction

Browse source 
Simplify boolean code.
This commit is contained in:
Nikolaj Bjorner 2018-12-07 18:59:45 +00:00 • committed by GitHub
commit f1d1e728ff
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 24 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_fpa.cpp
View file

@ -242,8 +242,8 @@ extern "C" {
RETURN_Z3(nullptr);
}
api::context * ctx = mk_c(c);
expr * a = negative != 0 ? ctx->fpautil().mk_ninf(to_sort(s)) :
ctx->fpautil().mk_pinf(to_sort(s));
expr * a = negative ? ctx->fpautil().mk_ninf(to_sort(s)) :
ctx->fpautil().mk_pinf(to_sort(s));
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(nullptr);
@ -259,8 +259,8 @@ extern "C" {
RETURN_Z3(nullptr);
}
api::context * ctx = mk_c(c);
expr * a = negative != 0 ? ctx->fpautil().mk_nzero(to_sort(s)) :
ctx->fpautil().mk_pzero(to_sort(s));
expr * a = negative ? ctx->fpautil().mk_nzero(to_sort(s)) :
ctx->fpautil().mk_pzero(to_sort(s));
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
Z3_CATCH_RETURN(nullptr);
@ -351,7 +351,7 @@ extern "C" {
ctx->fpautil().fm().set(tmp,
ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, exp, sig);
sgn, exp, sig);
expr * a = ctx->fpautil().mk_value(tmp);
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));
@ -371,7 +371,7 @@ extern "C" {
ctx->fpautil().fm().set(tmp,
ctx->fpautil().get_ebits(to_sort(ty)),
ctx->fpautil().get_sbits(to_sort(ty)),
sgn != 0, exp, sig);
sgn, exp, sig);
expr * a = ctx->fpautil().mk_value(tmp);
ctx->save_ast_trail(a);
RETURN_Z3(of_expr(a));

2
src/api/api_params.cpp
View file

@ -66,7 +66,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_params_set_bool(c, p, k, v);
RESET_ERROR_CODE();
to_params(p)->m_params.set_bool(norm_param_name(to_symbol(k)).c_str(), v != 0);
to_params(p)->m_params.set_bool(norm_param_name(to_symbol(k)).c_str(), v);
Z3_CATCH;
}

2
src/api/api_rcf.cpp
View file

@ -274,7 +274,7 @@ extern "C" {
RESET_ERROR_CODE();
reset_rcf_cancel(c);
std::ostringstream buffer;
rcfm(c).display(buffer, to_rcnumeral(a), compact != 0, html != 0);
rcfm(c).display(buffer, to_rcnumeral(a), compact, html);
return mk_c(c)->mk_external_string(buffer.str());
Z3_CATCH_RETURN("");
}

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

@ -505,7 +505,7 @@ namespace z3 {
out << Z3_ast_to_string(n.ctx(), n.m_ast); return out;
}
inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b) != 0; }
inline bool eq(ast const & a, ast const & b) { return Z3_is_eq_ast(a.ctx(), a, b); }
/**
@ -713,10 +713,10 @@ namespace z3 {
small integers, 64 bit integers or rational or decimal strings.
*/
bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
bool is_numeral_i64(int64_t& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u64(uint64_t& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_i64(int64_t& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u64(uint64_t& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
bool is_numeral(double& d) const { if (!is_numeral()) return false; d = Z3_get_numeral_double(ctx(), m_ast); check_error(); return true; }
@ -736,15 +736,15 @@ namespace z3 {
/**
\brief Return true if this expression is a universal quantifier.
*/
bool is_forall() const { return 0 != Z3_is_quantifier_forall(ctx(), m_ast); }
bool is_forall() const { return Z3_is_quantifier_forall(ctx(), m_ast); }
/**
\brief Return true if this expression is an existential quantifier.
*/
bool is_exists() const { return 0 != Z3_is_quantifier_exists(ctx(), m_ast); }
bool is_exists() const { return Z3_is_quantifier_exists(ctx(), m_ast); }
/**
\brief Return true if this expression is a lambda expression.
*/
bool is_lambda() const { return 0 != Z3_is_lambda(ctx(), m_ast); }
bool is_lambda() const { return Z3_is_lambda(ctx(), m_ast); }
/**
\brief Return true if this expression is a variable.
@ -753,12 +753,12 @@ namespace z3 {
/**
\brief Return true if expression is an algebraic number.
*/
bool is_algebraic() const { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
/**
\brief Return true if this expression is well sorted (aka type correct).
*/
bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast) != 0; check_error(); return r; }
bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; }
/**
\brief Return string representation of numeral or algebraic number
@ -2073,7 +2073,7 @@ namespace z3 {
// for function f.
bool has_interp(func_decl f) const {
check_context(*this, f);
return 0 != Z3_model_has_interp(ctx(), m_model, f);
return Z3_model_has_interp(ctx(), m_model, f);
}
func_interp add_func_interp(func_decl& f, expr& else_val) {
@ -2112,8 +2112,8 @@ namespace z3 {
}
unsigned size() const { return Z3_stats_size(ctx(), m_stats); }
std::string key(unsigned i) const { Z3_string s = Z3_stats_get_key(ctx(), m_stats, i); check_error(); return s; }
bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r != 0; }
bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r != 0; }
bool is_uint(unsigned i) const { bool r = Z3_stats_is_uint(ctx(), m_stats, i); check_error(); return r; }
bool is_double(unsigned i) const { bool r = Z3_stats_is_double(ctx(), m_stats, i); check_error(); return r; }
unsigned uint_value(unsigned i) const { unsigned r = Z3_stats_get_uint_value(ctx(), m_stats, i); check_error(); return r; }
double double_value(unsigned i) const { double r = Z3_stats_get_double_value(ctx(), m_stats, i); check_error(); return r; }
friend std::ostream & operator<<(std::ostream & out, stats const & s);
@ -2353,12 +2353,12 @@ namespace z3 {
unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }
bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal) != 0; }
bool inconsistent() const { return Z3_goal_inconsistent(ctx(), m_goal); }
unsigned depth() const { return Z3_goal_depth(ctx(), m_goal); }
void reset() { Z3_goal_reset(ctx(), m_goal); }
unsigned num_exprs() const { return Z3_goal_num_exprs(ctx(), m_goal); }
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal) != 0; }
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal) != 0; }
bool is_decided_sat() const { return Z3_goal_is_decided_sat(ctx(), m_goal); }
bool is_decided_unsat() const { return Z3_goal_is_decided_unsat(ctx(), m_goal); }
model convert_model(model const & m) const {
check_context(*this, m);
Z3_model new_m = Z3_goal_convert_model(ctx(), m_goal, m);