diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index 8774a4529..96f51731f 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -34,6 +34,7 @@ z3_add_component(lp nla_powers.cpp nla_solver.cpp nla_tangent_lemmas.cpp + nla_throttle.cpp nra_solver.cpp permutation_matrix.cpp random_updater.cpp diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4c79b5926..08b994644 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -37,10 +37,12 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_horner(this), m_grobner(this), m_emons(m_evars), + m_throttle(lra.trail()), m_use_nra_model(false), m_nra(s, m_nra_lim, *this) { m_nlsat_delay_bound = lp_settings().nlsat_delay(); + m_throttle.set_enabled(m_params.arith_nl_thrl()); lra.m_find_monics_with_changed_bounds_func = [&](const indexed_uint_set& columns_with_changed_bounds) { for (lpvar j : columns_with_changed_bounds) { if (is_monic_var(j)) diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index 46526b6a0..9ca96788a 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -28,6 +28,7 @@ #include "math/lp/nla_intervals.h" #include "nlsat/nlsat_solver.h" #include "params/smt_params_helper.hpp" +#include "math/lp/nla_throttle.h" namespace nra { class solver; @@ -102,6 +103,9 @@ class core { lpvar m_patched_var = 0; monic const* m_patched_monic = nullptr; + nla_throttle m_throttle; + bool m_throttle_enabled = true; + void check_weighted(unsigned sz, std::pair>* checks); @@ -432,6 +436,11 @@ public: void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); } void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); } + void set_throttle_enabled(bool enabled) { m_throttle_enabled = enabled; m_throttle.set_enabled(enabled); } + bool throttle_enabled() const { return m_throttle_enabled; } + nla_throttle& throttle() { return m_throttle; } + const nla_throttle& throttle() const { return m_throttle; } + }; // end of core struct pp_mon { diff --git a/src/math/lp/nla_throttle.cpp b/src/math/lp/nla_throttle.cpp new file mode 100644 index 000000000..0dbdce395 --- /dev/null +++ b/src/math/lp/nla_throttle.cpp @@ -0,0 +1,24 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Author: + Lev Nachmanson (levnach) + + --*/ +#include "math/lp/nla_throttle.h" +#include "util/trace.h" + +namespace nla { + +bool nla_throttle::insert_new_impl(const signature& sig) { + if (m_seen.contains(sig)) { + TRACE(nla_solver, tout << "throttled lemma generation\n";); + return true; // Already seen, throttle + } + + m_seen.insert(sig); + m_trail.push(insert_map(m_seen, sig)); + return false; // New, don't throttle +} + +} // namespace nla diff --git a/src/math/lp/nla_throttle.h b/src/math/lp/nla_throttle.h new file mode 100644 index 000000000..d3f923b81 --- /dev/null +++ b/src/math/lp/nla_throttle.h @@ -0,0 +1,112 @@ +/*++ + Copyright (c) 2017 Microsoft Corporation + + Author: + Lev Nachmanson (levnach) + + --*/ +#pragma once +#include "math/lp/nla_defs.h" +#include "util/hashtable.h" +#include "util/trail.h" +#include + +namespace nla { + +class nla_throttle { +public: + enum throttle_kind { + ORDER_LEMMA, // order lemma (9 params) + BINOMIAL_SIGN_LEMMA, // binomial sign (5 params) + MONOTONE_LEMMA // monotonicity (2 params) + }; + +private: + struct signature { + unsigned m_values[8]; + + signature() { + std::memset(m_values, 0, sizeof(m_values)); + } + + bool operator==(const signature& other) const { + return std::memcmp(m_values, other.m_values, sizeof(m_values)) == 0; + } + }; + + struct signature_hash { + unsigned operator()(const signature& s) const { + unsigned hash = 0; + for (int i = 0; i < 8; i++) { + hash = combine_hash(hash, s.m_values[i]); + } + return hash; + } + }; + + hashtable> m_seen; + trail_stack& m_trail; + bool m_enabled = true; + +public: + nla_throttle(trail_stack& trail) : m_trail(trail) {} + + void set_enabled(bool enabled) { m_enabled = enabled; } + bool enabled() const { return m_enabled; } + + // Monotone lemma: mvar + is_lt + bool insert_new(throttle_kind k, lpvar mvar, bool is_lt) { + if (!m_enabled) return false; + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(mvar); + sig.m_values[2] = static_cast(is_lt); + return insert_new_impl(sig); + } + + // Binomial sign: xy_var + x + y + sign + sy + bool insert_new(throttle_kind k, lpvar xy_var, lpvar x, lpvar y, int sign, int sy) { + if (!m_enabled) return false; + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(xy_var); + sig.m_values[2] = static_cast(x); + sig.m_values[3] = static_cast(y); + sig.m_values[4] = normalize_sign(sign); + sig.m_values[5] = normalize_sign(sy); + return insert_new_impl(sig); + } + + // Order lemma: ac_var + a + c_sign + c + bd_var + b_var + d_sign + d + ab_cmp + bool insert_new(throttle_kind k, lpvar ac_var, lpvar a, const rational& c_sign, lpvar c, + lpvar bd_var, lpvar b_var, const rational& d_sign, lpvar d, llc ab_cmp) { + if (!m_enabled) return false; + signature sig; + sig.m_values[0] = static_cast(k); + sig.m_values[1] = static_cast(ac_var); + sig.m_values[2] = static_cast(a); + sig.m_values[3] = pack_rational_sign(c_sign); + sig.m_values[4] = static_cast(c); + sig.m_values[5] = static_cast(bd_var); + sig.m_values[6] = static_cast(b_var); + // Pack d_sign, d, and ab_cmp into the last slot + sig.m_values[7] = (pack_rational_sign(d_sign) << 24) | + ((static_cast(d) & 0xFFFF) << 8) | + (static_cast(ab_cmp) & 0xFF); + return insert_new_impl(sig); + } + +private: + bool insert_new_impl(const signature& sig); + + // Helper functions for packing values + static unsigned pack_rational_sign(const rational& r) { + return r.is_pos() ? 1 : (r.is_neg() ? 255 : 0); + } + + static unsigned normalize_sign(int sign) { + return static_cast(sign + 127); + } +}; + +}