mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-16 07:45:27 +00:00
Code Activity

#5125

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-03-26 14:57:56 -07:00
parent c2b353ba72
commit e89071d366
2 changed files with 11 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -1236,6 +1236,7 @@ public:
mk_axiom(q_le_0, m_le_0); mk_axiom(q_le_0, m_le_0);
return; return;
} }
expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
#if 0 #if 0
expr_ref eqr(m.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p), m); expr_ref eqr(m.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p), m);
ctx().get_rewriter()(eqr); ctx().get_rewriter()(eqr);

20
src/util/mpq.cpp
View file

@ -185,8 +185,9 @@ void mpq_manager<SYNCH>::display_decimal(std::ostream & out, mpq const & a, unsi
template<bool SYNCH> template<bool SYNCH>
void mpq_manager<SYNCH>::set(mpq & a, char const * val) { void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
reset(a.m_num); reset(a.m_num);
mpz ten(10); _scoped_numeral<mpz_manager<SYNCH>> _zten(*this);
_scoped_numeral<mpz_manager<SYNCH> > tmp(*this); _scoped_numeral<mpz_manager<SYNCH>> tmp(*this);
set(_zten, 10);
char const * str = val; char const * str = val;
bool sign = false; bool sign = false;
while (str[0] == ' ') ++str; while (str[0] == ' ') ++str;
@ -195,7 +196,7 @@ void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
while (str[0] && (str[0] != '/') && (str[0] != '.') && (str[0] != 'e') && (str[0] != 'E')) { while (str[0] && (str[0] != '/') && (str[0] != '.') && (str[0] != 'e') && (str[0] != 'E')) {
if ('0' <= str[0] && str[0] <= '9') { if ('0' <= str[0] && str[0] <= '9') {
SASSERT(str[0] - '0' <= 9); SASSERT(str[0] - '0' <= 9);
mul(a.m_num, ten, tmp); mul(a.m_num, _zten, tmp);
add(tmp, this->mk_z(str[0] - '0'), a.m_num); add(tmp, this->mk_z(str[0] - '0'), a.m_num);
} }
++str; ++str;
@ -212,10 +213,10 @@ void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
reset(a.m_den); reset(a.m_den);
while (str[0] && (str[0] != 'e') && (str[0] != 'E')) { while (str[0] && (str[0] != 'e') && (str[0] != 'E')) {
if ('0' <= str[0] && str[0] <= '9') { if ('0' <= str[0] && str[0] <= '9') {
mul(a.m_den, ten, tmp); mul(a.m_den, _zten, tmp);
add(tmp, this->mk_z(str[0] - '0'), a.m_den); add(tmp, this->mk_z(str[0] - '0'), a.m_den);
if (!is_rat) if (!is_rat)
mul(tmp2, ten, tmp2); mul(tmp2, _zten, tmp2);
} }
++str; ++str;
} }
@ -250,17 +251,16 @@ void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
// a <- a.m_num + a.m_den/tmp2 // a <- a.m_num + a.m_den/tmp2
if (exp > static_cast<unsigned long long>(UINT_MAX)) if (exp > static_cast<unsigned long long>(UINT_MAX))
throw default_exception("exponent is too big"); throw default_exception("exponent is too big");
_scoped_numeral<mpq_manager<SYNCH> > b(*this); _scoped_numeral<mpq_manager<SYNCH>> b(*this);
if (has_den) { if (has_den) {
set(b, a.m_den, tmp2); set(b, a.m_den, tmp2);
set(a.m_den, 1); set(a.m_den, 1);
add(a, b, a); add(a, b, a);
} }
if (exp > 0) { if (exp > 0) {
_scoped_numeral<mpq_manager<SYNCH> > _exp(*this); _scoped_numeral<mpq_manager<SYNCH>> _exp(*this);
_scoped_numeral<mpq_manager<SYNCH> > _ten(*this); _scoped_numeral<mpq_manager<SYNCH>> _qten(*this);
set(_ten, 10); power(_qten, static_cast<unsigned>(exp), _exp);
power(_ten, static_cast<unsigned>(exp), _exp);
TRACE("mpq_set", tout << "a: " << to_string(a) << ", exp_sign:" << exp_sign << ", exp: " << exp << " " << to_string(_exp) << std::endl;); TRACE("mpq_set", tout << "a: " << to_string(a) << ", exp_sign:" << exp_sign << ", exp: " << exp << " " << to_string(_exp) << std::endl;);
if (exp_sign) if (exp_sign)
div(a, _exp, a); div(a, _exp, a);