From d3d0a5f635d305bbe8e27c0cdf33e9f33ab3f152 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 9 Nov 2023 13:03:14 +0100 Subject: [PATCH] compile --- src/math/polysat/interval.h | 2 +- src/math/polysat/viable.cpp | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/math/polysat/interval.h b/src/math/polysat/interval.h index 7e0b31bd0..7300b04b5 100644 --- a/src/math/polysat/interval.h +++ b/src/math/polysat/interval.h @@ -67,7 +67,7 @@ namespace polysat { // distance from a to b, wrapping around at mod_value. // basically mod(b - a, mod_value), but distance(0, mod_value, mod_value) = mod_value. - rational distance(rational const& a, rational const& b, rational const& mod_value) { + inline rational distance(rational const& a, rational const& b, rational const& mod_value) { SASSERT(mod_value.is_power_of_two()); SASSERT(0 <= a && a < mod_value); SASSERT(0 <= b && b <= mod_value); diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 93b2bf169..4c14c2dc4 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1435,6 +1435,7 @@ namespace polysat { e = n; } while (e != first); UNREACHABLE(); + return {nullptr, false}; } // find viable values in half-open interval [to_cover_lo;to_cover_hi[ w.r.t. unit intervals on the given layer @@ -1564,6 +1565,9 @@ namespace polysat { // TODO: refinement and fallback solver -- can we refine without throwing out all the entry_cursors we have set up? // we only have to chase intervals from the beginning if ec.cur has become inactive + + NOT_IMPLEMENTED_YET(); + return l_undef; } lbool viable::find_viable2(pvar v, rational& lo, rational& hi) {