From 651b41f8c075b2b48b0a4ff93aee497cda3eb1f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 13 Dec 2021 11:39:15 -0800 Subject: [PATCH] refactor fi functionality --- src/math/polysat/forbidden_intervals.cpp | 40 +++++++++++++++--------- src/math/polysat/forbidden_intervals.h | 14 +++++---- src/math/polysat/viable.cpp | 7 ++--- 3 files changed, 35 insertions(+), 26 deletions(-) diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index a71b7ccf6..ff77db9d7 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -61,11 +61,11 @@ namespace polysat { _backtrack.released = true; - if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond)) + if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi)) return true; - if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond)) + if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi)) return true; - if (match_linear3(c, a1, b1, e1, a2, b2, e2, fi.coeff, fi.interval, fi.side_cond)) + if (match_linear3(c, a1, b1, e1, a2, b2, e2, fi)) return true; _backtrack.released = false; @@ -157,17 +157,18 @@ namespace polysat { bool forbidden_intervals::match_linear1(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - rational& coeff, eval_interval& interval, vector& side_cond) { + fi_record& fi) { if (a2.is_zero() && !a1.is_zero()) { SASSERT(!a1.is_zero()); bool is_trivial = (b2 + 1).is_zero(); - push_eq(is_trivial, e2 + 1, side_cond); + push_eq(is_trivial, e2 + 1, fi.side_cond); auto lo = e2 - e1 + 1; rational lo_val = (b2 - b1 + 1).val(); auto hi = -e1; rational hi_val = (-b1).val(); - coeff = a1; - interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi); + fi.coeff = a1; + fi.interval = to_interval(c, is_trivial, fi.coeff, lo_val, lo, hi_val, hi); + add_non_unit_side_conds(fi, b1, e1, b2, e2); return true; } return false; @@ -180,17 +181,18 @@ namespace polysat { bool forbidden_intervals::match_linear2(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - rational& coeff, eval_interval& interval, vector& side_cond) { + fi_record& fi) { if (a1.is_zero() && !a2.is_zero()) { SASSERT(!a2.is_zero()); bool is_trivial = b1.is_zero(); - push_eq(is_trivial, e1, side_cond); + push_eq(is_trivial, e1, fi.side_cond); auto lo = -e2; rational lo_val = (-b2).val(); auto hi = e1 - e2; rational hi_val = (b1 - b2).val(); - coeff = a2; - interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi); + fi.coeff = a2; + fi.interval = to_interval(c, is_trivial, fi.coeff, lo_val, lo, hi_val, hi); + add_non_unit_side_conds(fi, b1, e1, b2, e2); return true; } return false; @@ -203,18 +205,26 @@ namespace polysat { bool forbidden_intervals::match_linear3(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - rational& coeff, eval_interval& interval, vector& side_cond) { + fi_record& fi) { if (a1 == a2 && !a1.is_zero()) { bool is_trivial = b1.val() == b2.val(); - push_eq(is_trivial, e1 - e2, side_cond); + push_eq(is_trivial, e1 - e2, fi.side_cond); auto lo = -e2; rational lo_val = (-b2).val(); auto hi = -e1; rational hi_val = (-b1).val(); - coeff = a1; - interval = to_interval(c, is_trivial, coeff, lo_val, lo, hi_val, hi); + fi.coeff = a1; + fi.interval = to_interval(c, is_trivial, fi.coeff, lo_val, lo, hi_val, hi); + add_non_unit_side_conds(fi, b1, e1, b2, e2); return true; } return false; } + + void forbidden_intervals::add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2) { + if (fi.coeff == 1) + return; + fi.side_cond.push_back(s.eq(b1, e1)); + fi.side_cond.push_back(s.eq(b2, e2)); + } } diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 99ceb7f92..6eef58eb0 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -30,20 +30,22 @@ namespace polysat { std::tuple linear_decompose(pvar v, pdd const& p, vector& out_side_cond); - bool match_linear1(signed_constraint const& c, - rational const & a1, pdd const& b1, pdd const& e1, - rational const & a2, pdd const& b2, pdd const& e2, - rational& coeff, eval_interval& interval, vector& side_cond); + bool match_linear1(signed_constraint const& c, + rational const& a1, pdd const& b1, pdd const& e1, + rational const& a2, pdd const& b2, pdd const& e2, + fi_record& fi); bool match_linear2(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - rational& coeff, eval_interval& interval, vector& side_cond); + fi_record& fi); bool match_linear3(signed_constraint const& c, rational const & a1, pdd const& b1, pdd const& e1, rational const & a2, pdd const& b2, pdd const& e2, - rational& coeff, eval_interval& interval, vector& side_cond); + fi_record& fi); + + void add_non_unit_side_conds(fi_record& fi, pdd const& b1, pdd const& e1, pdd const& b2, pdd const& e2); public: forbidden_intervals(solver& s) :s(s) {} diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index bbf47b722..ae5f5274a 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -252,15 +252,12 @@ namespace polysat { } LOG("forbidden interval " << e->coeff << " * " << e->interval << " [" << lo << ", " << hi << "["); SASSERT(hi <= max_value); + pdd lop = s.var2pdd(v).mk_val(lo); + pdd hip = s.var2pdd(v).mk_val(hi); entry* ne = alloc_entry(); ne->src = e->src; ne->side_cond = e->side_cond; - // TODO: have forbidden_interval.cpp add these side conditions for non-unit equalities and diseq_lin? - ne->side_cond.push_back(s.eq(e->interval.hi(), e->interval.hi_val())); - ne->side_cond.push_back(s.eq(e->interval.lo(), e->interval.lo_val())); ne->coeff = 1; - pdd lop = s.var2pdd(v).mk_val(lo); - pdd hip = s.var2pdd(v).mk_val(hi); ne->interval = eval_interval::proper(lop, lo, hip, hi); intersect(v, ne); return false;