mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
commit
fc7a217cd0
|
@ -909,6 +909,10 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
|
||||
RESET_ERROR_CODE();
|
||||
if (sgn == 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
|
||||
|
@ -968,6 +972,10 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
|
||||
RESET_ERROR_CODE();
|
||||
if (n == 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
|
||||
|
@ -1028,6 +1036,10 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
|
||||
RESET_ERROR_CODE();
|
||||
if (n == 0) {
|
||||
SET_ERROR_CODE(Z3_INVALID_ARG);
|
||||
return 0;
|
||||
}
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
|
||||
family_id fid = mk_c(c)->get_fpa_fid();
|
||||
|
|
|
@ -14,7 +14,7 @@ Author:
|
|||
Leonardo de Moura (leonardo) 2011-09-22
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
--*/
|
||||
#include"vector.h"
|
||||
#include"map.h"
|
||||
|
@ -30,7 +30,7 @@ void register_z3_replayer_cmds(z3_replayer & in);
|
|||
|
||||
void throw_invalid_reference() {
|
||||
TRACE("z3_replayer", tout << "invalid argument reference\n";);
|
||||
throw z3_replayer_exception("invalid argument reference1");
|
||||
throw z3_replayer_exception("invalid argument reference");
|
||||
}
|
||||
|
||||
struct z3_replayer::imp {
|
||||
|
@ -72,17 +72,17 @@ struct z3_replayer::imp {
|
|||
void check_arg(unsigned pos, value_kind k) const {
|
||||
if (pos >= m_args.size()) {
|
||||
TRACE("z3_replayer", tout << "too few arguments " << m_args.size() << " expecting " << kind2string(k) << "\n";);
|
||||
throw z3_replayer_exception("invalid argument reference2");
|
||||
throw z3_replayer_exception("invalid argument reference");
|
||||
}
|
||||
if (m_args[pos].m_kind != k) {
|
||||
std::stringstream strm;
|
||||
strm << "expecting " << kind2string(k) << " at position "
|
||||
strm << "expecting " << kind2string(k) << " at position "
|
||||
<< pos << " but got " << kind2string(m_args[pos].m_kind);
|
||||
throw z3_replayer_exception(strm.str().c_str());
|
||||
}
|
||||
}
|
||||
|
||||
struct value {
|
||||
struct value {
|
||||
value_kind m_kind;
|
||||
union {
|
||||
__int64 m_int;
|
||||
|
@ -129,7 +129,7 @@ struct z3_replayer::imp {
|
|||
break;
|
||||
case DOUBLE:
|
||||
out << v.m_double;
|
||||
break;
|
||||
break;
|
||||
case STRING:
|
||||
out << v.m_str;
|
||||
break;
|
||||
|
@ -160,7 +160,7 @@ struct z3_replayer::imp {
|
|||
char curr() const { return m_curr; }
|
||||
void new_line() { m_line++; }
|
||||
void next() { m_curr = m_stream.get(); }
|
||||
|
||||
|
||||
void read_string_core(char delimiter) {
|
||||
if (curr() != delimiter)
|
||||
throw z3_replayer_exception("invalid string/symbol");
|
||||
|
@ -258,7 +258,7 @@ struct z3_replayer::imp {
|
|||
}
|
||||
|
||||
bool is_double_char() const {
|
||||
return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E';
|
||||
return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E';
|
||||
}
|
||||
|
||||
#if (!defined(strtof))
|
||||
|
@ -376,7 +376,7 @@ struct z3_replayer::imp {
|
|||
}
|
||||
}
|
||||
else if (k == OBJECT) {
|
||||
TRACE("z3_replayer_bug",
|
||||
TRACE("z3_replayer_bug",
|
||||
tout << "args: "; display_args(tout); tout << "\n";
|
||||
tout << "push_back, sz: " << sz << ", m_obj_arrays.size(): " << m_obj_arrays.size() << "\n";
|
||||
for (unsigned i = asz - sz; i < asz; i++) {
|
||||
|
@ -421,7 +421,7 @@ struct z3_replayer::imp {
|
|||
break;
|
||||
case 'R':
|
||||
// reset
|
||||
next();
|
||||
next();
|
||||
TRACE("z3_replayer", tout << "[" << m_line << "] " << "R\n";);
|
||||
reset();
|
||||
break;
|
||||
|
@ -432,7 +432,7 @@ struct z3_replayer::imp {
|
|||
if (m_ptr == 0) {
|
||||
m_args.push_back(0);
|
||||
}
|
||||
else {
|
||||
else {
|
||||
void * obj = 0;
|
||||
if (!m_heap.find(m_ptr, obj))
|
||||
throw z3_replayer_exception("invalid pointer");
|
||||
|
@ -493,7 +493,7 @@ struct z3_replayer::imp {
|
|||
next(); skip_blank(); read_double();
|
||||
TRACE("z3_replayer", tout << "[" << m_line << "] " << "D " << m_double << "\n";);
|
||||
m_args.push_back(value(DOUBLE, m_double));
|
||||
break;
|
||||
break;
|
||||
case 'p':
|
||||
case 's':
|
||||
case 'u':
|
||||
|
@ -696,15 +696,15 @@ struct z3_replayer::imp {
|
|||
m_unsigned_arrays.reset();
|
||||
m_int_arrays.reset();
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
||||
z3_replayer::z3_replayer(std::istream & in) {
|
||||
m_imp = alloc(imp, *this, in);
|
||||
register_z3_replayer_cmds(*this);
|
||||
}
|
||||
|
||||
|
||||
z3_replayer::~z3_replayer() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue