From aaa587398ea84ec5107ae9906bf5d665da262ffd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2023 20:52:34 -0700 Subject: [PATCH 1/3] add propagation flag to monic and method for updating it to emonics. This replaces the bool-vector tracking for propagation and internalizes it to the emonics class Signed-off-by: Nikolaj Bjorner --- src/math/lp/emonics.cpp | 16 ++++++++++++++++ src/math/lp/emonics.h | 2 ++ src/math/lp/monic.h | 3 +++ 3 files changed, 21 insertions(+) diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index a8ac63689..f051a8f2e 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -595,4 +595,20 @@ bool emonics::invariant() const { return true; } + +void emonics::set_propagated(monic& m) { + struct set_unpropagated : public trail { + emonics& em; + unsigned var; + public: + set_unpropagated(emonics& em, unsigned var): em(em), var(var) {} + void undo() override { + em[var].set_propagated(false); + } + }; + SASSERT(!m.is_propagated()); + m.set_propagated(true); + m_u_f_stack.push(set_unpropagated(*this, m.var())); +} + } diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h index e4f4f4848..051e1d6f0 100644 --- a/src/math/lp/emonics.h +++ b/src/math/lp/emonics.h @@ -142,6 +142,8 @@ public: void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} + void set_propagated(monic& m); + // this method is required by union_find trail_stack & get_trail_stack() { return m_u_f_stack; } diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h index 884adaaf8..d981b2042 100644 --- a/src/math/lp/monic.h +++ b/src/math/lp/monic.h @@ -58,6 +58,7 @@ class monic: public mon_eq { svector m_rvars; bool m_rsign; mutable unsigned m_visited; + bool m_propagated = false; public: // constructors monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx): @@ -74,6 +75,8 @@ public: void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); } void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); } void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); } + void set_propagated(bool p) { m_propagated = p; } + bool is_propagated() const { return m_propagated; } svector::const_iterator begin() const { return vars().begin(); } svector::const_iterator end() const { return vars().end(); } From 6559e5fb321c67530f5276751023575d86017953 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2023 21:15:07 -0700 Subject: [PATCH 2/3] port over std_vector and std-allocator functionality from monomial propagation branch Signed-off-by: Nikolaj Bjorner --- src/util/memory_manager.h | 23 +++++++++++++++++++++++ src/util/vector.h | 3 +++ 2 files changed, 26 insertions(+) diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 7dab520df..af56c4507 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -128,6 +128,29 @@ void dealloc_svect(T * ptr) { memory::deallocate(ptr); } +template +struct std_allocator { + using value_type = T; + // the constructors must be provided according to cpp docs + std_allocator() = default; + template constexpr std_allocator(const std_allocator&) noexcept {} + + + T* allocate(std::size_t n) { + return static_cast(memory::allocate(n * sizeof(T))); + } + + void deallocate(T* p, std::size_t n) { + memory::deallocate(p); + } +}; + +// the comparison operators must be provided according to cpp docs +template +bool operator==(const std_allocator&, const std_allocator&) { return true; } +template +bool operator!=(const std_allocator&, const std_allocator&) { return false; } + struct mem_stat { }; diff --git a/src/util/vector.h b/src/util/vector.h index 1cb25a8c4..55b52d745 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -33,6 +33,7 @@ Revision History: #include "util/memory_manager.h" #include "util/hash.h" #include "util/z3_exception.h" +#include // disable warning for constant 'if' expressions. // these are used heavily in templates. @@ -40,6 +41,8 @@ Revision History: #pragma warning(disable:4127) #endif +template +using std_vector = std::vector>; #if 0 From 2297b0334b14a0141dd0a26d4d2942f83bb28ad9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2023 23:53:14 -0700 Subject: [PATCH 3/3] re-introduce simple implementation of linear monomial propagation for evaluation Signed-off-by: Nikolaj Bjorner --- src/math/lp/emonics.cpp | 4 +-- src/math/lp/emonics.h | 2 +- src/math/lp/monomial_bounds.cpp | 55 ++++++++++++++++++++------------- src/math/lp/monomial_bounds.h | 1 - src/math/lp/nla_core.cpp | 7 +---- src/smt/theory_lra.cpp | 2 +- src/util/util.h | 8 +++++ 7 files changed, 47 insertions(+), 32 deletions(-) diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp index f051a8f2e..9a9e4566b 100644 --- a/src/math/lp/emonics.cpp +++ b/src/math/lp/emonics.cpp @@ -596,7 +596,7 @@ bool emonics::invariant() const { } -void emonics::set_propagated(monic& m) { +void emonics::set_propagated(monic const& m) { struct set_unpropagated : public trail { emonics& em; unsigned var; @@ -607,7 +607,7 @@ void emonics::set_propagated(monic& m) { } }; SASSERT(!m.is_propagated()); - m.set_propagated(true); + (*this)[m.var()].set_propagated(true); m_u_f_stack.push(set_unpropagated(*this, m.var())); } diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h index 051e1d6f0..fe0b19117 100644 --- a/src/math/lp/emonics.h +++ b/src/math/lp/emonics.h @@ -142,7 +142,7 @@ public: void merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} void after_merge_eh(unsigned r2, unsigned r1, unsigned v2, unsigned v1) {} - void set_propagated(monic& m); + void set_propagated(monic const& m); // this method is required by union_find trail_stack & get_trail_stack() { return m_u_f_stack; } diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 84af29d05..8e4ed6cef 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -263,40 +263,53 @@ namespace nla { unit_propagate(m); } + void monomial_bounds::unit_propagate(monic const& m) { - m_propagated.reserve(m.var() + 1, false); - if (m_propagated[m.var()]) + if (m.is_propagated()) return; if (!is_linear(m)) return; - - c().trail().push(set_bitvector_trail(m_propagated, m.var())); + + c().m_emons.set_propagated(m); rational k = fixed_var_product(m); - new_lemma lemma(c(), "fixed-values"); if (k == 0) { - for (auto v : m) { - if (c().var_is_fixed(v) && c().val(v).is_zero()) { - lemma.explain_fixed(v); - break; - } - } - lemma |= ineq(m.var(), lp::lconstraint_kind::EQ, 0); + ineq ineq(m.var(), lp::lconstraint_kind::EQ, 0); + if (c().ineq_holds(ineq)) + return; + + lpvar zero_var = find(m, [&](lpvar v) { return c().var_is_fixed(v) && c().val(v).is_zero(); }); + + IF_VERBOSE(2, verbose_stream() << "zero " << m.var() << "\n"); + + new_lemma lemma(c(), "fixed-values"); + lemma.explain_fixed(zero_var); + lemma |= ineq; } else { + lpvar w = non_fixed_var(m); + lp::lar_term term; + term.add_monomial(m.rat_sign(), m.var()); + + if (w != null_lpvar) { + IF_VERBOSE(2, verbose_stream() << "linear " << m.var() << " " << k << " " << w << "\n"); + term.add_monomial(-k, w); + k = 0; + } + else + IF_VERBOSE(2, verbose_stream() << "fixed " << m.var() << " " << k << "\n"); + + ineq ineq(term, lp::lconstraint_kind::EQ, k); + if (c().ineq_holds(ineq)) + return; + + new_lemma lemma(c(), "linearized-fixed-values"); for (auto v : m) if (c().var_is_fixed(v)) - lemma.explain_fixed(v); - - lpvar w = non_fixed_var(m); - SASSERT(w != null_lpvar); - - lp::lar_term term; - term.add_monomial(-m.rat_sign(), m.var()); - term.add_monomial(k, w); - lemma |= ineq(term, lp::lconstraint_kind::EQ, 0); + lemma.explain_fixed(v); + lemma |= ineq; } } diff --git a/src/math/lp/monomial_bounds.h b/src/math/lp/monomial_bounds.h index c728d1a4c..74c61dd5f 100644 --- a/src/math/lp/monomial_bounds.h +++ b/src/math/lp/monomial_bounds.h @@ -31,7 +31,6 @@ namespace nla { bool is_zero(lpvar v) const; // monomial propagation - bool_vector m_propagated; void unit_propagate(monic const& m); bool is_linear(monic const& m); rational fixed_var_product(monic const& m); diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 4990a087c..f147640b8 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1811,13 +1811,8 @@ bool core::improve_bounds() { } void core::propagate() { - // disable for now - return; - // propagate linear monomials - m_lemmas.reset(); - + m_lemmas.reset(); m_monomial_bounds.unit_propagate(); - } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index ae658b105..fb84b265d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2149,9 +2149,9 @@ public: case l_true: propagate_basic_bounds(); propagate_bounds_with_lp_solver(); + // propagate_nla(); break; case l_undef: - propagate_nla(); break; } return true; diff --git a/src/util/util.h b/src/util/util.h index 1e2310eb3..275374512 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -378,6 +378,14 @@ bool all_of(S const& set, T const& p) { return true; } +template +R find(S const& set, std::function p) { + for (auto const& s : set) + if (p(s)) + return s; + throw default_exception("element not found"); +} + /** \brief Iterator for the [0..sz[0]) X [0..sz[1]) X ... X [0..sz[n-1]). it contains the current value.