From 482738bc8a08e7abd0abaa7030261aa5255a984d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Jan 2018 15:51:45 -0800 Subject: [PATCH] avoid reset_error in dec_ref in bv_val #1443. Add BSD required template instance #1444 Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 6 ++++++ src/api/api_context.h | 2 +- src/api/api_numeral.cpp | 4 ++-- src/api/c++/z3++.h | 10 +++++----- src/util/lp/lp_solver_instances.cpp | 1 + 5 files changed, 15 insertions(+), 8 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 23ac62a66..8299c136c 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -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. diff --git a/src/api/api_context.h b/src/api/api_context.h index 58893d1c1..a2321d7fe 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -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 diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 9a778d6e0..1cee7469c 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -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(); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b1e667e9f..808382561 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -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 _bits(n); for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0; diff --git a/src/util/lp/lp_solver_instances.cpp b/src/util/lp/lp_solver_instances.cpp index 4fe04c05f..599a0a8bc 100644 --- a/src/util/lp/lp_solver_instances.cpp +++ b/src/util/lp/lp_solver_instances.cpp @@ -34,6 +34,7 @@ template void lp::lp_solver::print_statistics_on_A(std::ostream template bool lp::lp_solver::problem_is_empty(); template void lp::lp_solver::scale(); template void lp::lp_solver::set_scaled_cost(unsigned int); +template std::string lp::lp_solver::get_column_name(unsigned int) const; template lp::lp_solver::~lp_solver(); template void lp::lp_solver::add_constraint(lp::lp_relation, lp::mpq, unsigned int); template void lp::lp_solver::cleanup();