From ec2e9105d3f4907df64e3b0e6205db12569dcbd6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Aug 2021 17:08:08 -0700 Subject: [PATCH] include paths Signed-off-by: Nikolaj Bjorner --- src/math/bigfix/Hacl_Bignum256.h | 10 ++++---- src/math/polysat/fixplex.h | 10 ++++---- src/math/polysat/fixplex_def.h | 39 ++++++++++++------------------ src/math/polysat/linear_solver.cpp | 7 ++---- src/math/polysat/linear_solver.h | 10 ++++---- 5 files changed, 33 insertions(+), 43 deletions(-) diff --git a/src/math/bigfix/Hacl_Bignum256.h b/src/math/bigfix/Hacl_Bignum256.h index db7c99b78..783d7d09a 100644 --- a/src/math/bigfix/Hacl_Bignum256.h +++ b/src/math/bigfix/Hacl_Bignum256.h @@ -29,13 +29,13 @@ extern "C" { #endif -#include "kremlin/internal/types.h" -#include "kremlin/lowstar_endianness.h" +#include "math/bigfix/internal/types.h" +#include "math/bigfix/kremlin/lowstar_endianness.h" #include -#include "kremlin/internal/target.h" +#include "math/bigfix/kremlin/internal/target.h" -#include "Hacl_Bignum.h" -#include "Hacl_Bignum_Base.h" +#include "math/bigfix/Hacl_Bignum.h" +#include "math/bigfix/Hacl_Bignum_Base.h" /******************************************************************************* diff --git a/src/math/polysat/fixplex.h b/src/math/polysat/fixplex.h index d0f94ff91..4ed1347a2 100644 --- a/src/math/polysat/fixplex.h +++ b/src/math/polysat/fixplex.h @@ -47,7 +47,7 @@ namespace polysat { virtual void add_le(var_t v, var_t w, unsigned dep) = 0; virtual void add_lt(var_t v, var_t w, unsigned dep) = 0; virtual void restore_ineq() = 0; - virtual void get_infeasible_deps(unsigned_vector& deps) = 0; + virtual unsigned_vector const& get_unsat_core() const = 0; }; @@ -160,7 +160,7 @@ namespace polysat { unsigned m_blands_rule_threshold { 1000 }; random_gen m_random; uint_set m_left_basis; - unsigned m_infeasible_var { null_var }; + unsigned_vector m_unsat_core; unsigned_vector m_base_vars; stats m_stats; vector m_stashed_bounds; @@ -211,12 +211,10 @@ namespace polysat { void add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs); - void get_infeasible_deps(unsigned_vector& deps) override; + unsigned_vector const& get_unsat_core() const override { return m_unsat_core; } private: - row get_infeasible_row(); - std::ostream& display_row(std::ostream& out, row const& r, bool values = true); var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; } @@ -267,6 +265,8 @@ namespace polysat { void check_blands_rule(var_t v, unsigned& num_repeated); pivot_strategy_t pivot_strategy() { return m_bland ? S_BLAND : S_DEFAULT; } var_t select_error_var(bool least); + void set_infeasible_base(var_t v); + void set_infeasible_bounds(var_t v); // facilities for handling inequalities void add_ineq(var_t v, var_t w, unsigned dep, bool strict); diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 2ce807b58..805583bdf 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -97,7 +97,7 @@ namespace polysat { lbool fixplex::make_feasible() { ++m_stats.m_num_checks; m_left_basis.reset(); - m_infeasible_var = null_var; + m_unsat_core.reset(); unsigned num_iterations = 0; unsigned num_repeated = 0; var_t v = null_var; @@ -114,7 +114,7 @@ namespace polysat { break; case l_false: m_to_patch.insert(v); - m_infeasible_var = v; + set_infeasible_base(v); ++m_stats.m_num_infeasible; return l_false; case l_undef: @@ -792,32 +792,22 @@ namespace polysat { return true; } - template - typename fixplex::row - fixplex::get_infeasible_row() { - SASSERT(is_base(m_infeasible_var)); - return base2row(m_infeasible_var); - } - /*** - * Extract dependencies for infeasible row. - * A safe approximation is to extract dependencies for all bounds. - * - * Different modes of infeasibility may not be based on a row: - * - inequalities - * - parity constraints between two rows. + * Record an infeasible row. */ template - void fixplex::get_infeasible_deps(unsigned_vector& deps) { - auto row = get_infeasible_row(); + void fixplex::set_infeasible_base(var_t v) { + m_unsat_core.reset(); + SASSERT(is_base(v)); + auto row = base2row(v); for (auto const& e : M.row_entries(row)) { var_t v = e.var(); auto lo = m_vars[v].m_lo_dep; auto hi = m_vars[v].m_hi_dep; if (lo != UINT_MAX) - deps.push_back(lo); + m_unsat_core.push_back(lo); if (hi != UINT_MAX) - deps.push_back(hi); + m_unsat_core.push_back(hi); } } @@ -1164,8 +1154,10 @@ namespace polysat { mod_interval r(l, h); bool was_fixed = lo(x) + 1 == hi(x); m_vars[x] &= r; - if (m_vars[x].is_empty()) - m_infeasible_var = x; + if (m_vars[x].is_empty()) { + // TODO + IF_VERBOSE(0, verbose_stream() << "infeasible\n"); + } else if (!was_fixed && lo(x) + 1 == hi(x)) { // TBD: track based on inequality not row // fixed_var_eh(r, x); @@ -1179,8 +1171,9 @@ namespace polysat { 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()) - m_infeasible_var = x; + if (m_vars[x].is_empty()) { + IF_VERBOSE(0, verbose_stream() << "infeasible\n"); + } else if (!was_fixed && lo(x) + 1 == hi(x)) fixed_var_eh(r, x); } diff --git a/src/math/polysat/linear_solver.cpp b/src/math/polysat/linear_solver.cpp index 2549b5586..aae17304f 100644 --- a/src/math/polysat/linear_solver.cpp +++ b/src/math/polysat/linear_solver.cpp @@ -313,15 +313,12 @@ namespace polysat { SASSERT(m_unsat_f); deps.reset(); cs.reset(); - m_unsat_f->get_infeasible_deps(deps); - unsigned j = 0; - for (unsigned dep : deps) { + for (unsigned dep : m_unsat_f->get_unsat_core()) { if (is_constraint_dep(dep)) cs.push_back(m_active[dep2constraint_idx(dep)]); else - deps[j++] = dep2external_dep(dep); + deps.push_back(dep2external_dep(dep)); } - deps.shrink(j); } // current value assigned to (linear) variable according to tableau. diff --git a/src/math/polysat/linear_solver.h b/src/math/polysat/linear_solver.h index 51bc05fc0..8472a0721 100644 --- a/src/math/polysat/linear_solver.h +++ b/src/math/polysat/linear_solver.h @@ -111,11 +111,11 @@ namespace polysat { // unsigned_vector var2mono(unsigned sz, var_t v) { throw default_exception("nyi"); } // distinguish constraint and justification dependencies - unsigned external_dep2dep(unsigned dep) const { return UINT_MAX - dep; } - unsigned constraint_idx2dep(unsigned idx) const { return idx; } - bool is_constraint_dep(unsigned dep) const { return dep < UINT_MAX / 2; } - unsigned dep2constraint_idx(unsigned dep) const { return dep; } - unsigned dep2external_dep(unsigned dep) const { return UINT_MAX - dep; } + unsigned external_dep2dep(unsigned dep) const { return dep * 2; } + unsigned constraint_idx2dep(unsigned idx) const { return 1 + (idx * 2); } + bool is_constraint_dep(unsigned dep) const { return 0 != (dep & 0x1); } + unsigned dep2constraint_idx(unsigned dep) const { return dep >> 2; } + unsigned dep2external_dep(unsigned dep) const { return dep >> 2; } public: linear_solver(solver& s):