diff --git a/src/math/bigfix/lib_intrinsics.h b/src/math/bigfix/lib_intrinsics.h index cf269bb89..7a8cf2f48 100644 --- a/src/math/bigfix/lib_intrinsics.h +++ b/src/math/bigfix/lib_intrinsics.h @@ -2,9 +2,6 @@ #include -#if __has_include("config.h") -#include "config.h" -#endif #if defined(COMPILE_INTRINSICS) #if defined(_MSC_VER) @@ -16,7 +13,7 @@ #if !defined(COMPILE_INTRINSICS) -#include "Hacl_IntTypes_Intrinsics.h" +#include "math/bigfix/Hacl_IntTypes_Intrinsics.h" #define Lib_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4) \ (Hacl_IntTypes_Intrinsics_add_carry_u32(x1, x2, x3, x4)) diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h index 4ed1347a2..a43f06e18 100644 --- a/src/math/polysat/fixplex.h +++ b/src/math/polysat/fixplex.h @@ -204,7 +204,7 @@ namespace polysat { void set_max_iterations(unsigned n) { m_max_iterations = n; } unsigned get_num_vars() const { return m_vars.size(); } void reset(); - void propagate_bounds(); + lbool propagate_bounds(); void propagate_eqs(); vector const& var_eqs() const { return m_var_eqs; } void reset_eqs() { m_var_eqs.reset(); } @@ -230,11 +230,11 @@ namespace polysat { void get_offset_eqs(row const& r); void fixed_var_eh(row const& r, var_t x); void eq_eh(var_t x, var_t y, row const& r1, row const& r2); - void propagate_bounds(row const& r); - void propagate_bounds(ineq const& i); - void new_bound(row const& r, var_t x, mod_interval const& range); - void new_bound(ineq const& i, var_t x, numeral const& lo, numeral const& hi); - void conflict_bound(ineq const& i); + lbool propagate_bounds(row const& r); + lbool propagate_bounds(ineq const& i); + lbool new_bound(row const& r, var_t x, mod_interval const& range); + lbool new_bound(ineq const& i, var_t x, numeral const& lo, numeral const& hi); + lbool conflict_bound(ineq const& i); void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value); numeral value2delta(var_t v, numeral const& new_value) const; numeral value2error(var_t v, numeral const& new_value) const; diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 18cb7b121..45d889079 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -1052,11 +1052,16 @@ namespace polysat { template - void fixplex::propagate_bounds() { - for (unsigned i = 0; i < m_rows.size(); ++i) - propagate_bounds(row(i)); - for (auto ineq : m_ineqs) - propagate_bounds(ineq); + lbool fixplex::propagate_bounds() { + lbool r = l_true; + for (unsigned i = 0; r == l_true && i < m_rows.size(); ++i) + r = propagate_bounds(row(i)); + for (auto ineq : m_ineqs) { + if (r != l_true) + break; + r = propagate_bounds(ineq); + } + return r; } /** @@ -1069,7 +1074,7 @@ namespace polysat { */ template - void fixplex::propagate_bounds(row const& r) { + lbool fixplex::propagate_bounds(row const& r) { mod_interval range(0, 1); numeral free_c = 0; var_t free_v = null_var; @@ -1078,33 +1083,36 @@ namespace polysat { numeral const& c = e.coeff(); if (is_free(v)) { if (free_v != null_var) - return; + return l_true; free_v = v; free_c = c; continue; } range += m_vars[v] * c; if (range.is_free()) - return; + return l_true; } if (free_v != null_var) { range = (-range) * free_c; - new_bound(r, free_v, range); + lbool res = new_bound(r, free_v, range); SASSERT(in_bounds(free_v)); - return; + return res; } for (auto const& e : M.row_entries(r)) { var_t v = e.var(); SASSERT(!is_free(v)); auto range1 = range - m_vars[v] * e.coeff(); - new_bound(r, v, range1); + lbool res = new_bound(r, v, range1); + if (res != l_true) + return res; // SASSERT(in_bounds(v)); } + return l_true; } template - void fixplex::propagate_bounds(ineq const& i) { + lbool fixplex::propagate_bounds(ineq const& i) { // v < w & lo(v) + 1 = 0 -> conflict // v < w & hi(w) = 0 -> conflict // v < w & lo(v) >= hi(w) -> conflict @@ -1116,65 +1124,71 @@ namespace polysat { var_t v = i.v, w = i.w; bool s = i.strict; if (s && lo(v) + 1 == 0) - conflict_bound(i); + return conflict_bound(i); else if (s && hi(w) == 0) - conflict_bound(i); + return conflict_bound(i); else if (s && lo(v) >= hi(w)) - conflict_bound(i); + return conflict_bound(i); else if (!s && lo(v) > hi(w)) - conflict_bound(i); + return conflict_bound(i); else if (s && hi(v) >= hi(w)) { SASSERT(lo(v) < hi(w)); SASSERT(hi(w) != 0); - new_bound(i, v, lo(v), hi(w) - 1); + return new_bound(i, v, lo(v), hi(w) - 1); } else if (s && lo(v) >= lo(w)) { SASSERT(lo(v) + 1 != 0); SASSERT(hi(w) > lo(v)); - new_bound(i, w, lo(v) + 1, hi(w)); + return new_bound(i, w, lo(v) + 1, hi(w)); } else if (!s && hi(v) > hi(w)) { SASSERT(lo(v) <= hi(w)); - new_bound(i, v, lo(v), hi(w)); + return new_bound(i, v, lo(v), hi(w)); } else if (!s && lo(v) > lo(w)) { SASSERT(lo(v) <= hi(w)); - new_bound(i, w, lo(v), hi(w)); + return new_bound(i, w, lo(v), hi(w)); } + return l_true; } template - void fixplex::conflict_bound(ineq const& i) { + lbool fixplex::conflict_bound(ineq const& i) { NOT_IMPLEMENTED_YET(); + return l_false; } template - void fixplex::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h) { + lbool fixplex::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h) { mod_interval r(l, h); bool was_fixed = lo(x) + 1 == hi(x); m_vars[x] &= r; if (m_vars[x].is_empty()) { // TODO IF_VERBOSE(0, verbose_stream() << "infeasible\n"); + return l_false; } else if (!was_fixed && lo(x) + 1 == hi(x)) { // TBD: track based on inequality not row // fixed_var_eh(r, x); } + return l_true; } template - void fixplex::new_bound(row const& r, var_t x, mod_interval const& range) { + lbool fixplex::new_bound(row const& r, var_t x, mod_interval const& range) { if (range.is_free()) - return; + return l_true; bool was_fixed = lo(x) + 1 == hi(x); m_vars[x] &= range; IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n"); if (m_vars[x].is_empty()) { IF_VERBOSE(0, verbose_stream() << "infeasible\n"); + return l_false; } else if (!was_fixed && lo(x) + 1 == hi(x)) fixed_var_eh(r, x); + return l_true; } template