#include "sat/smt/euf_solver.h"
#include "sat/smt/arith_solver.h"
namespace arith {
void solver::mk_div_axiom(expr* p, expr* q) {
if (a.is_zero(q)) return;
literal eqz = eq_internalize(q, a.mk_real(0));
literal eq = eq_internalize(a.mk_mul(q, a.mk_div(p, q)), p);
add_clause(eqz, eq);
}
void solver::mk_to_int_axiom(app* n) {
expr* x = nullptr, * y = nullptr;
VERIFY(a.is_to_int(n, x));
if (a.is_to_real(x, y)) {
literal eq = eq_internalize(y, n);
add_clause(eq);
}
else {
expr_ref to_r(a.mk_to_real(n), m);
expr_ref lhs(a.mk_sub(to_r, x), m);
expr_ref rhs(a.mk_real(0), m);
expr_ref lo(a.mk_le(lhs, rhs), m);
expr_ref lhs1(a.mk_sub(x, to_r), m);
expr_ref rhs1(a.mk_real(1), m);
expr_ref hi(a.mk_ge(lhs1, rhs1), m);
literal llo = mk_literal(lo);
literal lhi = mk_literal(hi);
add_clause(llo);
add_clause(~lhi);
}
}
void solver::mk_abs_axiom(app* n) {
expr* x = nullptr;
VERIFY(a.is_abs(n, x));
literal is_nonneg = mk_literal(a.mk_ge(x, a.mk_numeral(rational::zero(), n->get_sort())));
add_clause(~is_nonneg, eq_internalize(n, x));
add_clause(is_nonneg, eq_internalize(n, a.mk_uminus(x)));
}
void solver::mk_power0_axioms(app* t, app* n) {
expr_ref p0(a.mk_power0(n, t->get_arg(1)), m);
literal eq = eq_internalize(n, a.mk_numeral(rational(0), a.is_int(n)));
add_clause(~eq, eq_internalize(t, p0));
add_clause(eq, eq_internalize(t, a.mk_numeral(rational(1), a.is_int(t))));
}
void solver::mk_power_axiom(expr* p, expr* x, expr* y) {
if (a.is_zero(y)) {
mk_power0_axioms(to_app(p), to_app(x));
return;
}
rational r;
if (a.is_extended_numeral(x, r) && r > 0) {
expr_ref zero(a.mk_real(0), m);
add_clause(~mk_literal(a.mk_le(p, zero)));
}
if (a.is_extended_numeral(y, r) && r > 0) {
if (denominator(r) > 1) {
expr_ref x_ge_0(a.mk_ge(x, a.mk_real(0)), m);
expr_ref xn(x, m);
if (numerator(r) > 1)
xn = a.mk_power(x, a.mk_real(numerator(r)));
expr_ref x_eq_pn(a.mk_eq(xn, a.mk_power(p, a.mk_real(denominator(r)))), m);
add_clause(~mk_literal(x_ge_0), mk_literal(x_eq_pn));
}
}
}
void solver::mk_is_int_axiom(expr* n) {
expr* x = nullptr;
VERIFY(a.is_is_int(n, x));
expr_ref lhs(a.mk_to_real(a.mk_to_int(x)), m);
literal eq = eq_internalize(lhs, x);
literal is_int = ctx.expr2literal(n);
add_equiv(is_int, eq);
}
void solver::mk_idiv_mod_axioms(expr* p, expr* q) {
if (a.is_zero(q)) {
return;
}
TRACE(arith, tout << expr_ref(p, m) << " " << expr_ref(q, m) << "\n";);
expr_ref div(a.mk_idiv(p, q), m);
expr_ref mod(a.mk_mod(p, q), m);
expr_ref zero(a.mk_int(0), m);
if (a.is_zero(p)) {
literal q_ge_0 = mk_literal(a.mk_ge(q, zero));
literal q_le_0 = mk_literal(a.mk_le(q, zero));
literal d_ge_0 = mk_literal(a.mk_ge(div, zero));
literal d_le_0 = mk_literal(a.mk_le(div, zero));
literal m_ge_0 = mk_literal(a.mk_ge(mod, zero));
literal m_le_0 = mk_literal(a.mk_le(mod, zero));
add_clause(q_ge_0, d_ge_0);
add_clause(q_ge_0, d_le_0);
add_clause(q_ge_0, m_ge_0);
add_clause(q_ge_0, m_le_0);
add_clause(q_le_0, d_ge_0);
add_clause(q_le_0, d_le_0);
add_clause(q_le_0, m_ge_0);
add_clause(q_le_0, m_le_0);
return;
}
literal eq = eq_internalize(a.mk_add(a.mk_mul(q, div), mod), p);
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
rational k(0);
expr_ref upper(m);
if (a.is_numeral(q, k)) {
if (k.is_pos()) {
upper = a.mk_numeral(k - 1, true);
}
else if (k.is_neg()) {
upper = a.mk_numeral(-k - 1, true);
}
}
else {
k = rational::zero();
}
if (!k.is_zero()) {
add_clause(eq);
add_clause(mod_ge_0);
add_clause(mk_literal(a.mk_le(mod, upper)));
}
else {
expr_ref mone(a.mk_int(-1), m);
expr_ref non_negative(a.mk_ge(q, zero), m);
expr_ref neg_q(a.mk_uminus(q), m);
expr_ref abs_q(m.mk_ite(non_negative, q, neg_q), m);
literal eqz = mk_literal(m.mk_eq(q, zero));
literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero));
literal mod_lt_q = mk_literal(a.mk_le(a.mk_sub(mod, abs_q), mone));
add_clause(eqz, eq);
add_clause(eqz, mod_ge_0);
add_clause(eqz, mod_lt_q);
if (!a.is_uminus(q))
add_clause(mk_literal(m.mk_eq(mod, a.mk_mod(p, a.mk_uminus(q)))));
#if 0#endif
if (a.is_zero(p)) {
add_clause(eqz, mk_literal(m.mk_eq(mod, zero)));
add_clause(eqz, mk_literal(m.mk_eq(div, zero)));
}
else if (!a.is_numeral(q)) {
add_clause(eqz, mk_literal(a.mk_le(a.mk_mul(q, div), p)));
}
}
if (get_config().m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
unsigned _k = k.get_unsigned();
literal_vector lits;
for (unsigned j = 0; j < _k; ++j) {
literal mod_j = eq_internalize(mod, a.mk_int(j));
lits.push_back(mod_j);
}
add_clause(lits);
}
}
void solver::mk_rem_axiom(expr* dividend, expr* divisor) {
expr_ref zero(a.mk_int(0), m);
expr_ref rem(a.mk_rem(dividend, divisor), m);
expr_ref mod(a.mk_mod(dividend, divisor), m);
expr_ref mmod(a.mk_uminus(mod), m);
expr_ref degz_expr(a.mk_ge(divisor, zero), m);
literal dgez = mk_literal(degz_expr);
literal pos = eq_internalize(rem, mod);
literal neg = eq_internalize(rem, mmod);
add_clause(~dgez, pos);
add_clause(dgez, neg);
}
bool solver::check_bv_term(app* n) {
unsigned sz = 0;
expr* _x = nullptr, * _y = nullptr;
if (!ctx.is_relevant(expr2enode(n)))
return true;
expr_ref vx(m), vy(m),vn(m);
rational valn, valx, valy;
bool is_int;
VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
if (!get_value(expr2enode(_x), vx) || !get_value(expr2enode(_y), vy) || !get_value(expr2enode(n), vn)) {
IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
found_unsupported(n);
return true;
}
if (!a.is_numeral(vn, valn, is_int) || !is_int || !a.is_numeral(vx, valx, is_int) || !is_int || !a.is_numeral(vy, valy, is_int) || !is_int) {
IF_VERBOSE(2, verbose_stream() << "could not get value of " << mk_pp(n, m) << "\n");
found_unsupported(n);
return true;
}
rational N = rational::power_of_two(sz);
valx = mod(valx, N);
valy = mod(valy, N);
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
SASSERT(0 <= valn && valn < N);
auto bitof = [&](expr* x, unsigned i) {
expr_ref r(m);
expr_ref low_bits(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), m);
r = a.mk_ge(low_bits, a.mk_int(rational::power_of_two(i)));
return mk_literal(r);
};
if (a.is_band(n)) {
IF_VERBOSE(2, verbose_stream() << "band: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << "&" << valy << "\n");
for (unsigned i = 0; i < sz; ++i) {
bool xb = valx.get_bit(i);
bool yb = valy.get_bit(i);
bool nb = valn.get_bit(i);
if (xb && yb && !nb) {
literal xbit = bitof(x, i);
literal ybit = bitof(y, i);
literal nbit = bitof(n, i);
add_clause(~xbit, ~ybit, nbit);
}
else if (nb && !xb) {
literal nbit = bitof(n, i);
literal xbit = bitof(x, i);
add_clause(~nbit, xbit);
}
else if (nb && !yb) {
literal nbit = bitof(n, i);
literal ybit = bitof(y, i);
add_clause(~nbit, ybit);
}
else
continue;
return false;
}
}
if (a.is_shl(n)) {
SASSERT(valy >= 0);
if (valy >= sz || valy == 0)
return true;
unsigned k = valy.get_unsigned();
expr_ref lhs(a.mk_mul(_x, a.mk_int(rational::power_of_two(k))), m);
expr_ref rhs(a.mk_int(N), m);
sat::literal eq = eq_internalize(n, a.mk_mod(lhs, rhs));
if (s().value(eq) == l_true)
return true;
add_clause(~eq_internalize(y, a.mk_int(k)), eq);
IF_VERBOSE(2, verbose_stream() << "shl: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " << " << valy << "\n");
return false;
}
if (a.is_lshr(n)) {
SASSERT(valy >= 0);
if (valy >= sz || valy == 0)
return true;
unsigned k = valy.get_unsigned();
sat::literal eq = eq_internalize(n, a.mk_idiv(x, a.mk_int(rational::power_of_two(k))));
if (s().value(eq) == l_true)
return true;
add_clause(~eq_internalize(y, a.mk_int(k)), eq);
IF_VERBOSE(2, verbose_stream() << "lshr: " << mk_bounded_pp(n, m) << " " << valn << " := " << valx << " >>l " << valy << "\n");
return false;
}
if (a.is_ashr(n)) {
SASSERT(valy >= 0);
if (valy >= sz || valy == 0)
return true;
unsigned k = valy.get_unsigned();
sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
sat::literal eq;
expr* xdiv2k;
switch (s().value(signx)) {
case l_true:
xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
{
expr_ref lhs(a.mk_add(xdiv2k, a.mk_int(-rational::power_of_two(sz - k))), m);
expr_ref rhs(a.mk_int(N), m);
eq = eq_internalize(n, a.mk_mod(lhs, rhs));
}
if (s().value(eq) == l_true)
return true;
break;
case l_false:
xdiv2k = a.mk_idiv(x, a.mk_int(rational::power_of_two(k)));
eq = eq_internalize(n, xdiv2k);
if (s().value(eq) == l_true)
return true;
break;
case l_undef:
ctx.mark_relevant(signx);
return false;
}
add_clause(~eq_internalize(y, a.mk_int(k)), ~signx, eq);
return false;
}
return true;
}
bool solver::check_bv_terms() {
for (app* n : m_bv_terms) {
if (!check_bv_term(n)) {
++m_stats.m_bv_axioms;
return false;
}
}
return true;
}
void solver::mk_bv_axiom(app* n) {
unsigned sz = 0;
expr* _x = nullptr, * _y = nullptr;
VERIFY(a.is_band(n, sz, _x, _y) || a.is_shl(n, sz, _x, _y) || a.is_ashr(n, sz, _x, _y) || a.is_lshr(n, sz, _x, _y));
rational N = rational::power_of_two(sz);
expr_ref x(a.mk_mod(_x, a.mk_int(N)), m);
expr_ref y(a.mk_mod(_y, a.mk_int(N)), m);
add_clause(mk_literal(a.mk_ge(n, a.mk_int(0))));
add_clause(mk_literal(a.mk_le(n, a.mk_int(N - 1))));
if (a.is_band(n)) {
add_clause(mk_literal(a.mk_le(n, x)));
add_clause(mk_literal(a.mk_le(n, y)));
}
else if (a.is_shl(n)) {
literal large_shift = mk_literal(a.mk_ge(y, a.mk_int(sz)));
literal result_zero = mk_literal(m.mk_eq(n, a.mk_int(0)));
add_clause(~large_shift, result_zero);
literal zero_shift = mk_literal(a.mk_eq(y, a.mk_int(0)));
literal unchanged = mk_literal(m.mk_eq(n, x));
add_clause(~zero_shift, unchanged);
}
else if (a.is_lshr(n)) {
literal large_shift = mk_literal(a.mk_ge(y, a.mk_int(sz)));
literal result_zero = mk_literal(m.mk_eq(n, a.mk_int(0)));
add_clause(~large_shift, result_zero);
literal zero_shift = mk_literal(a.mk_eq(y, a.mk_int(0)));
literal unchanged = mk_literal(m.mk_eq(n, x));
add_clause(~zero_shift, unchanged);
}
else if (a.is_ashr(n)) {
auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2)));
literal large_shift;
{
expr_ref amount(a.mk_mod(y, a.mk_int(N)), m);
large_shift = mk_literal(a.mk_ge(amount, a.mk_int(sz)));
}
literal result_zero = mk_literal(m.mk_eq(n, a.mk_int(0)));
add_clause(~large_shift, signx, result_zero);
{
expr_ref lhs(a.mk_mod(y, a.mk_int(N)), m);
expr_ref rhs(a.mk_int(sz), m);
literal large_shift = mk_literal(a.mk_ge(lhs, rhs));
literal result_minus_one = mk_literal(m.mk_eq(n, a.mk_int(N - 1)));
add_clause(~large_shift, ~signx, result_minus_one);
}
expr_ref lhs(a.mk_mod(y, a.mk_int(N)), m);
expr_ref rhs(a.mk_int(0), m);
literal zero_shift = mk_literal(a.mk_eq(lhs, rhs));
literal unchanged = mk_literal(m.mk_eq(n, x));
add_clause(~zero_shift, unchanged);
}
else
UNREACHABLE();
}
void solver::mk_bound_axioms(api_bound& b) {
theory_var v = b.get_var();
lp_api::bound_kind kind1 = b.get_bound_kind();
rational const& k1 = b.get_value();
lp_bounds& bounds = m_bounds[v];
api_bound* end = nullptr;
api_bound* lo_inf = end, * lo_sup = end;
api_bound* hi_inf = end, * hi_sup = end;
for (api_bound* other : bounds) {
if (other == &b) continue;
if (b.get_lit() == other->get_lit()) continue;
lp_api::bound_kind kind2 = other->get_bound_kind();
rational const& k2 = other->get_value();
if (k1 == k2 && kind1 == kind2) {
continue;
}
SASSERT(k1 != k2 || kind1 != kind2);
if (kind2 == lp_api::lower_t) {
if (k2 < k1) {
if (lo_inf == end || k2 > lo_inf->get_value()) {
lo_inf = other;
}
}
else if (lo_sup == end || k2 < lo_sup->get_value()) {
lo_sup = other;
}
}
else if (k2 < k1) {
if (hi_inf == end || k2 > hi_inf->get_value()) {
hi_inf = other;
}
}
else if (hi_sup == end || k2 < hi_sup->get_value()) {
hi_sup = other;
}
}
if (lo_inf != end) mk_bound_axiom(b, *lo_inf);
if (lo_sup != end) mk_bound_axiom(b, *lo_sup);
if (hi_inf != end) mk_bound_axiom(b, *hi_inf);
if (hi_sup != end) mk_bound_axiom(b, *hi_sup);
}
void solver::add_farkas_clause(sat::literal l1, sat::literal l2) {
arith_proof_hint* bound_params = nullptr;
if (ctx.use_drat()) {
m_arith_hint.set_type(ctx, hint_type::farkas_h);
m_arith_hint.add_lit(rational(1), ~l1);
m_arith_hint.add_lit(rational(1), ~l2);
bound_params = m_arith_hint.mk(ctx);
}
add_clause(l1, l2, bound_params);
}
void solver::mk_bound_axiom(api_bound& b1, api_bound& b2) {
literal l1(b1.get_lit());
literal l2(b2.get_lit());
rational const& k1 = b1.get_value();
rational const& k2 = b2.get_value();
lp_api::bound_kind kind1 = b1.get_bound_kind();
lp_api::bound_kind kind2 = b2.get_bound_kind();
bool v_is_int = b1.is_int();
SASSERT(b1.get_var() == b2.get_var());
if (k1 == k2 && kind1 == kind2) return;
SASSERT(k1 != k2 || kind1 != kind2);
if (kind1 == lp_api::lower_t) {
if (kind2 == lp_api::lower_t) {
if (k2 <= k1)
add_farkas_clause(~l1, l2);
else
add_farkas_clause(l1, ~l2);
}
else if (k1 <= k2)
add_farkas_clause(l1, l2);
else {
add_farkas_clause(~l1, ~l2);
if (v_is_int && k1 == k2 + rational(1))
add_farkas_clause(l1, l2);
}
}
else if (kind2 == lp_api::lower_t) {
if (k1 >= k2)
add_farkas_clause(l1, l2);
else {
add_farkas_clause(~l1, ~l2);
if (v_is_int && k1 == k2 - rational(1))
add_farkas_clause(l1, l2);
}
}
else {
if (k1 >= k2)
add_farkas_clause(l1, ~l2);
else
add_farkas_clause(~l1, l2);
}
}
api_bound* solver::mk_var_bound(sat::literal lit, theory_var v, lp_api::bound_kind bk, rational const& bound) {
scoped_internalize_state st(*this);
st.vars().push_back(v);
st.coeffs().push_back(rational::one());
init_left_side(st);
lp::constraint_index cT, cF;
bool v_is_int = is_int(v);
auto vi = register_theory_var_in_lar_solver(v);
lp::lconstraint_kind kT = bound2constraint_kind(v_is_int, bk, true);
lp::lconstraint_kind kF = bound2constraint_kind(v_is_int, bk, false);
cT = lp().mk_var_bound(vi, kT, bound);
if (v_is_int) {
rational boundF = (bk == lp_api::lower_t) ? bound - 1 : bound + 1;
cF = lp().mk_var_bound(vi, kF, boundF);
}
else {
cF = lp().mk_var_bound(vi, kF, bound);
}
add_ineq_constraint(cT, lit);
add_ineq_constraint(cF, ~lit);
return alloc(api_bound, lit, v, vi, v_is_int, bound, bk, cT, cF);
}
lp::lconstraint_kind solver::bound2constraint_kind(bool is_int, lp_api::bound_kind bk, bool is_true) {
switch (bk) {
case lp_api::lower_t:
return is_true ? lp::GE : (is_int ? lp::LE : lp::LT);
case lp_api::upper_t:
return is_true ? lp::LE : (is_int ? lp::GE : lp::GT);
}
UNREACHABLE();
return lp::EQ;
}
void solver::new_eq_eh(euf::th_eq const& e) {
theory_var v1 = e.v1();
theory_var v2 = e.v2();
if (is_bool(v1) || a.is_complex(var2expr(v1)))
return;
force_push();
expr* e1 = var2expr(v1);
expr* e2 = var2expr(v2);
TRACE(arith, tout << "new eq: v" << v1 << " v" << v2 << "\n";);
if (e1->get_id() > e2->get_id())
std::swap(e1, e2);
if (m.are_equal(e1, e2))
return;
++m_stats.m_assert_eq;
m_new_eq = true;
euf::enode* n1 = var2enode(v1);
euf::enode* n2 = var2enode(v2);
lpvar w1 = register_theory_var_in_lar_solver(v1);
lpvar w2 = register_theory_var_in_lar_solver(v2);
if (lp().are_equal(w1, w2))
return;
auto cs = lp().add_equality(w1, w2);
add_eq_constraint(cs.first, n1, n2);
add_eq_constraint(cs.second, n1, n2);
}
void solver::new_diseq_eh(euf::th_eq const& e) {
if (a.is_complex(var2expr(e.v1())))
return;
TRACE(artih, tout << mk_bounded_pp(e.eq()->get_expr(), m) << "\n");
ensure_column(e.v1());
ensure_column(e.v2());
m_delayed_eqs.push_back(std::make_pair(e, false));
ctx.push(push_back_vector<svector<std::pair<euf::th_eq, bool>>>(m_delayed_eqs));
}
void solver::mk_diseq_axiom(theory_var v1, theory_var v2) {
if (is_bool(v1))
return;
force_push();
expr* e1 = var2expr(v1);
expr* e2 = var2expr(v2);
if (e1->get_id() > e2->get_id())
std::swap(e1, e2);
if (m.are_distinct(e1, e2))
return;
literal le, ge;
if (a.is_numeral(e1))
std::swap(e1, e2);
SASSERT(!a.is_numeral(e1));
literal eq = eq_internalize(e1, e2);
if (a.is_numeral(e2)) {
le = mk_literal(a.mk_le(e1, e2));
ge = mk_literal(a.mk_ge(e1, e2));
}
else {
expr_ref diff(a.mk_sub(e1, e2), m);
expr_ref zero(a.mk_numeral(rational(0), a.is_int(e1)), m);
rewrite(diff);
if (a.is_numeral(diff)) {
if (!a.is_zero(diff))
return;
if (a.is_zero(diff))
add_unit(eq);
else
add_unit(~eq);
return;
}
le = mk_literal(a.mk_le(diff, zero));
ge = mk_literal(a.mk_ge(diff, zero));
}
++m_stats.m_assert_diseq;
add_farkas_clause(~eq, le);
add_farkas_clause(~eq, ge);
add_clause(~le, ~ge, eq, explain_trichotomy(le, ge, eq));
}
void solver::assert_idiv_mod_axioms(theory_var u, theory_var v, theory_var w, rational const& r) {
app_ref term(m);
term = a.mk_mul(a.mk_numeral(r, true), var2expr(w));
term = a.mk_add(var2expr(v), term);
term = a.mk_sub(var2expr(u), term);
theory_var z = internalize_def(term);
lpvar zi = register_theory_var_in_lar_solver(z);
lpvar vi = register_theory_var_in_lar_solver(v);
add_def_constraint_and_equality(zi, lp::GE, rational::zero());
add_def_constraint_and_equality(zi, lp::LE, rational::zero());
add_def_constraint_and_equality(vi, lp::GE, rational::zero());
add_def_constraint_and_equality(vi, lp::LT, abs(r));
SASSERT(!is_infeasible());
TRACE(arith, tout << term << "\n" << lp().constraints(););
}
bool solver::check_idiv_bounds() {
if (m_idiv_terms.empty()) {
return true;
}
bool all_divs_valid = true;
for (unsigned i = 0; i < m_idiv_terms.size(); ++i) {
expr* n = m_idiv_terms[i];
expr* p = nullptr, * q = nullptr;
VERIFY(a.is_idiv(n, p, q));
theory_var v1 = internalize_def(p);
ensure_column(v1);
lp::impq r1 = get_ivalue(v1);
rational r2;
if (!r1.x.is_int() || r1.x.is_neg() || !r1.y.is_zero()) {
continue;
}
if (a.is_numeral(q, r2) && r2.is_pos()) {
if (!a.is_bounded(n)) {
TRACE(arith, tout << "unbounded " << expr_ref(n, m) << "\n";);
continue;
}
theory_var v = internalize_def(n);
lp::impq val_v = get_ivalue(v);
if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue;
TRACE(arith, tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";);
rational div_r = div(r1.x, r2);
rational mul(1);
rational hi = r2 * div_r + r2 - 1;
rational lo = r2 * div_r;
expr* n1 = nullptr, * n2 = nullptr;
if (a.is_mul(p, n1, n2) && a.is_extended_numeral(n1, mul) && mul.is_pos()) {
p = n2;
hi = floor(hi / mul);
lo = ceil(lo / mul);
}
literal p_le_r1 = mk_literal(a.mk_le(p, a.mk_numeral(hi, true)));
literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(lo, true)));
literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div_r, true)));
literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div_r, true)));
add_clause(~p_le_r1, n_le_div);
add_clause(~p_ge_r1, n_ge_div);
all_divs_valid = false;
TRACE(arith, tout << r1 << " div " << r2 << "\n";);
continue;
}
}
return all_divs_valid;
}
void solver::fixed_var_eh(theory_var v, u_dependency* dep, rational const& bound) {
theory_var w = euf::null_theory_var;
enode* x = var2enode(v);
if (bound.is_zero())
w = lp().local_to_external(get_zero(a.is_int(x->get_expr())));
else if (bound.is_one())
w = lp().local_to_external(get_one(a.is_int(x->get_expr())));
else if (!m_value2var.find(bound, w))
return;
enode* y = var2enode(w);
if (x->get_sort() != y->get_sort())
return;
if (x->get_root() == y->get_root())
return;
reset_evidence();
m_explanation.clear();
for (auto ci : lp().flatten(dep))
consume(rational::one(), ci);
++m_stats.m_fixed_eqs;
auto* hint = explain_implied_eq(m_explanation, x, y);
auto* jst = euf::th_explain::propagate(*this, m_core, m_eqs, x, y, hint);
ctx.propagate(x, y, jst->to_index());
}
}