diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index 822d7dcc4..b75a1fdd7 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -296,11 +296,8 @@ namespace polysat { return false; } - if (conflict_var() == v) { - forbidden_intervals fi(s); - if (fi.perform(v, cjust_v, *this)) - return true; - } + if (conflict_var() == v && s.m_forbidden_intervals.perform(v, cjust_v, *this)) + return true; m_vars.remove(v); diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index a557f77c5..46220c748 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -17,6 +17,7 @@ Author: --*/ #include "math/polysat/forbidden_intervals.h" #include "math/polysat/interval.h" +#include "math/polysat/solver.h" #include "math/polysat/log.h" namespace polysat { @@ -219,6 +220,8 @@ namespace polysat { return true; if (match_linear4(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond)) return true; + if (match_linear5(c, a1, b1, e1, a2, b2, e2, out_interval, out_side_cond)) + return true; _backtrack.released = false; return false; @@ -386,16 +389,27 @@ namespace polysat { } /** + * Ad-hoc linear forbidden intervals * ax <= b, b != -1, a < b: x not in [ceil((b+1)/a) .. floor((2^K-1)/a)] * b <= ax, 0 < a < b: x not in [0 .. floor((b-1)/a)] * ax < b, a < b: x not in [ceil(b/a) .. floor((2^K-1)/a)] * b < ax, 0 < a <= b: x not in [0 .. floor(b/a)] + * + * TODO: generalize to ax + b <= c scenarios where ax does not overflow + * and ax+b does not overflow, but is larger than c + * Scenarios: + * - ax + b <= c + * - ax + b < c + * - c <= ax + b + * - c < ax + b */ bool forbidden_intervals::match_linear5(signed_constraint const& c, rational const& a1, pdd const& b1, pdd const& e1, rational const& a2, pdd const& b2, pdd const& e2, eval_interval& interval, vector& side_cond) { auto& m = e1.manager(); + + // ax <= b, b != -1, a < b: x not in [ceil((b+1)/a) .. floor((2^K-1)/a)] if (c.is_positive() && !a1.is_zero() && !a1.is_one() && a2.is_zero() && b1.is_zero() && e2.is_val() && @@ -404,11 +418,14 @@ namespace polysat { side_cond.push_back(s.eq(e1)); auto lo_val = ceil((b2.val() + 1) / a1); auto hi_val = floor(m.max_value() / a1) + 1; + SASSERT(lo_val < hi_val); auto lo = m.mk_val(lo_val); auto hi = m.mk_val(hi_val); interval = eval_interval::proper(lo, lo_val, hi, hi_val); return true; } + + // b <= ax, 0 < a < b: x not in [0 .. floor((b-1)/a)] if (c.is_positive() && !a2.is_zero() && !a2.is_one() && a1.is_zero() && b2.is_zero() && @@ -417,15 +434,39 @@ namespace polysat { side_cond.push_back(s.eq(e2)); auto lo_val = rational::zero(); auto hi_val = floor((b1.val() - 1) / a2) + 1; + SASSERT(lo_val < hi_val); auto lo = m.mk_val(lo_val); auto hi = m.mk_val(hi_val); interval = eval_interval::proper(lo, lo_val, hi, hi_val); return true; } - if (c.is_negative() && - !a2.is_zero() && !a2.is_one() && - a1.is_zero() && false) { + // ax < b, a < b: x not in [ceil(b/a) .. floor((2^K-1)/a)] + if (c.is_negative() && + !a2.is_zero() && !a2.is_one() && b2.is_zero() && + a1.is_zero() && e1.is_val() && a2 < b1.val()) { + if (!e2.is_val()) + side_cond.push_back(s.eq(e2)); + auto lo_val = ceil(b1.val() / a2); + auto hi_val = floor(m.max_value() / a2) + 1; + auto lo = m.mk_val(lo_val); + auto hi = m.mk_val(hi_val); + interval = eval_interval::proper(lo, lo_val, hi, hi_val); + return true; + } + + // b < ax, 0 < a <= b: x not in [0 .. floor(b/a)] + if (c.is_negative() && + !a1.is_zero() && !a1.is_one() && b1.is_zero() && + a2.is_zero() && e2.is_val() && a1 <= b2.val()) { + if (!e1.is_val()) + side_cond.push_back(s.eq(e2)); + auto lo_val = rational::zero(); + auto hi_val = floor(b2.val() / a1) + 1; + auto lo = m.mk_val(lo_val); + auto hi = m.mk_val(hi_val); + interval = eval_interval::proper(lo, lo_val, hi, hi_val); + return true; } return false; } diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h index 25d46071c..2eaec2920 100644 --- a/src/math/polysat/forbidden_intervals.h +++ b/src/math/polysat/forbidden_intervals.h @@ -14,11 +14,12 @@ Author: --*/ #pragma once -#include "math/polysat/constraint.h" -#include "math/polysat/solver.h" +#include "math/polysat/conflict.h" namespace polysat { + class solver; + class forbidden_intervals { solver& s; void revert_core(conflict& core); diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp index e6d3d56b5..3f186e0e7 100644 --- a/src/math/polysat/saturation.cpp +++ b/src/math/polysat/saturation.cpp @@ -367,7 +367,7 @@ namespace polysat { /// [z] z <= y' /\ zx > yx ==> Ω*(x,y') \/ y'x > yx /// [z] z <= y' /\ yx <= zx ==> Ω*(x,y') \/ yx <= y'x bool inf_saturate::try_ugt_z(pvar z, conflict& core, inequality const& yx_l_zx) { - set_rule("[z] z <= y' /\ zx > yx"); + set_rule("[z] z <= y' && zx > yx"); pdd y = s.var(z); pdd x = y; if (!is_YX_l_zX(z, yx_l_zx, x, y)) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 8a532b616..7a84b72bc 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -19,7 +19,6 @@ Author: #include "math/polysat/solver.h" #include "math/polysat/explain.h" #include "math/polysat/log.h" -#include "math/polysat/forbidden_intervals.h" #include "math/polysat/variable_elimination.h" // For development; to be removed once the linear solver works well enough @@ -39,6 +38,7 @@ namespace polysat { m_viable(*this), m_linear_solver(*this), m_conflict(*this), + m_forbidden_intervals(*this), m_bvars(), m_free_pvars(m_activity), m_constraints(m_bvars) { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 8bcd7349f..19743ee16 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -29,6 +29,7 @@ Author: #include "math/polysat/justification.h" #include "math/polysat/linear_solver.h" #include "math/polysat/search_state.h" +#include "math/polysat/forbidden_intervals.h" #include "math/polysat/trail.h" #include "math/polysat/viable.h" #include "math/polysat/log.h" @@ -71,6 +72,7 @@ namespace polysat { scoped_ptr_vector m_pdd; linear_solver m_linear_solver; conflict m_conflict; + forbidden_intervals m_forbidden_intervals; bool_var_manager m_bvars; // Map boolean variables to constraints var_queue m_free_pvars; // free poly vars stats m_stats; diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 0fc81a8cd..a954c01d0 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -168,8 +168,6 @@ namespace polysat { */ bool has_viable(pvar v); - bool is_false(pvar v) { return !has_viable(v); } - /** * check if value is viable according to m_viable. */