mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Add GCD test
This commit is contained in:
parent
b7b7970c4a
commit
6506d33b35
|
@ -65,7 +65,7 @@ protected:
|
|||
|
||||
void set_curr_sort(sort * s) { m_curr_sort = s; }
|
||||
|
||||
expr * const * get_monomials(expr * & t, unsigned & sz) {
|
||||
expr * const * get_monomials(expr * & t, unsigned & sz) const {
|
||||
if (is_add(t)) {
|
||||
sz = to_app(t)->get_num_args();
|
||||
return to_app(t)->get_args();
|
||||
|
@ -86,7 +86,7 @@ protected:
|
|||
bool hoist_multiplication(expr_ref& som);
|
||||
expr* merge_muls(expr* x, expr* y);
|
||||
|
||||
bool is_mul(expr * t, numeral & c, expr * & pp);
|
||||
bool is_mul(expr * t, numeral & c, expr * & pp) const;
|
||||
|
||||
class mon_lt {
|
||||
poly_rewriter& rw;
|
||||
|
@ -124,6 +124,8 @@ public:
|
|||
bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
|
||||
bool is_zero(expr* e) const;
|
||||
|
||||
bool gcd_test(expr* lhs, expr* rhs) const;
|
||||
|
||||
|
||||
br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
|
||||
SASSERT(num_args > 0);
|
||||
|
|
|
@ -445,7 +445,7 @@ inline expr * poly_rewriter<Config>::get_power_product(expr * t, numeral & a) {
|
|||
}
|
||||
|
||||
template<typename Config>
|
||||
bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) {
|
||||
bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) const {
|
||||
if (!is_mul(t) || to_app(t)->get_num_args() != 2)
|
||||
return false;
|
||||
if (!is_numeral(to_app(t)->get_arg(0), c))
|
||||
|
@ -454,6 +454,42 @@ bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) {
|
|||
return true;
|
||||
}
|
||||
|
||||
template<typename Config>
|
||||
bool poly_rewriter<Config>::gcd_test(expr* lhs, expr* rhs) const {
|
||||
numeral g(0), offset(0), c;
|
||||
expr* t = nullptr;
|
||||
unsigned sz = 0;
|
||||
expr* const* args = get_monomials(lhs, sz);
|
||||
auto test = [&](bool side, expr* e) {
|
||||
if (is_numeral(e, c)) {
|
||||
if (!c.is_int())
|
||||
return false;
|
||||
if (side)
|
||||
offset += c;
|
||||
else
|
||||
offset -= c;
|
||||
return true;
|
||||
}
|
||||
else if (is_mul(e, c, t)) {
|
||||
if (!c.is_int() || c.is_zero())
|
||||
return false;
|
||||
g = gcd(abs(c), g);
|
||||
return !g.is_one();
|
||||
}
|
||||
return false;
|
||||
};
|
||||
for (unsigned i = 0; i < sz; ++i)
|
||||
if (!test(true, args[i]))
|
||||
return true;
|
||||
args = get_monomials(rhs, sz);
|
||||
for (unsigned i = 0; i < sz; ++i)
|
||||
if (!test(false, args[i]))
|
||||
return true;
|
||||
if (!offset.is_zero() && !g.is_zero() && !divides(g, offset))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
template<typename Config>
|
||||
bool poly_rewriter<Config>::mon_lt::operator()(expr* e1, expr * e2) const {
|
||||
|
|
|
@ -387,8 +387,11 @@ public:
|
|||
}
|
||||
|
||||
friend inline std::ostream & operator<<(std::ostream & target, rational const & r) {
|
||||
target << m().to_string(r.m_val);
|
||||
return target;
|
||||
return target << m().to_string(r.m_val);
|
||||
}
|
||||
|
||||
friend inline bool divides(rational const& a, rational const& b) {
|
||||
return m().divides(a.to_mpq(), b.to_mpq());
|
||||
}
|
||||
|
||||
friend inline rational gcd(rational const & r1, rational const & r2);
|
||||
|
|
Loading…
Reference in a new issue