mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

avoid reset_error in dec_ref in bv_val #1443. Add BSD required template instance #1444

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-07 15:51:45 -08:00
parent 711023d557
commit 482738bc8a
5 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_context.cpp
View file

@ -152,6 +152,12 @@ namespace api {
}
}
void context::reset_error_code() {
m_error_code = Z3_OK;
}
void context::check_searching() {
if (m_searching) {
set_error_code(Z3_INVALID_USAGE); // TBD: error code could be fixed.

2
src/api/api_context.h
View file

@ -138,7 +138,7 @@ namespace api {
datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
Z3_error_code get_error_code() const { return m_error_code; }
void reset_error_code() { m_error_code = Z3_OK; }
void reset_error_code();
void set_error_code(Z3_error_code err);
void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
// Sign an error if solver is searching

4
src/api/api_numeral.cpp
View file

@ -73,7 +73,7 @@ extern "C" {
('P' == *m) ||
('+' == *m))))) {
SET_ERROR_CODE(Z3_PARSER_ERROR);
return 0;
RETURN_Z3(0);
}
++m;
}
@ -235,7 +235,7 @@ extern "C" {
expr* e = to_expr(a);
if (!e) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return "";
RETURN_Z3("");
}
rational r;
arith_util & u = mk_c(c)->autil();

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

@ -2524,11 +2524,11 @@ namespace z3 {
inline expr context::real_val(__uint64 n) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
inline expr context::real_val(char const * n) { Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }
inline expr context::bv_val(int n, unsigned sz) { Z3_ast r = Z3_mk_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(unsigned n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(__int64 n, unsigned sz) { Z3_ast r = Z3_mk_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(__uint64 n, unsigned sz) { Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(char const * n, unsigned sz) { Z3_ast r = Z3_mk_numeral(m_ctx, n, bv_sort(sz)); check_error(); return expr(*this, r); }
inline expr context::bv_val(int n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::bv_val(unsigned n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::bv_val(__int64 n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::bv_val(__uint64 n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::bv_val(char const * n, unsigned sz) { sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }
inline expr context::bv_val(unsigned n, bool const* bits) {
array<Z3_bool> _bits(n);
for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;

1
src/util/lp/lp_solver_instances.cpp
View file

@ -34,6 +34,7 @@ template void lp::lp_solver<double, double>::print_statistics_on_A(std::ostream
template bool lp::lp_solver<double, double>::problem_is_empty();
template void lp::lp_solver<double, double>::scale();
template void lp::lp_solver<double, double>::set_scaled_cost(unsigned int);
template std::string lp::lp_solver<double, double>::get_column_name(unsigned int) const;
template lp::lp_solver<double, double>::~lp_solver();
template void lp::lp_solver<lp::mpq, lp::mpq>::add_constraint(lp::lp_relation, lp::mpq, unsigned int);
template void lp::lp_solver<lp::mpq, lp::mpq>::cleanup();