From a0df8507d9a2c3973cc9eb579ad2634402e62926 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 12 Jun 2023 21:13:20 +0200 Subject: [PATCH] extract/concat slicing wip --- src/math/polysat/CMakeLists.txt | 2 + src/math/polysat/naming.cpp | 65 +++++++++ src/math/polysat/naming.h | 65 +++++++++ src/math/polysat/slicing.cpp | 225 ++++++++++++++++++++++++++++++++ src/math/polysat/slicing.h | 154 ++++++++++++++++++++++ src/math/polysat/solver.cpp | 6 +- src/math/polysat/solver.h | 15 +++ 7 files changed, 531 insertions(+), 1 deletion(-) create mode 100644 src/math/polysat/naming.cpp create mode 100644 src/math/polysat/naming.h create mode 100644 src/math/polysat/slicing.cpp create mode 100644 src/math/polysat/slicing.h diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt index 6b3e97aff..9e411c346 100644 --- a/src/math/polysat/CMakeLists.txt +++ b/src/math/polysat/CMakeLists.txt @@ -13,6 +13,7 @@ z3_add_component(polysat justification.cpp linear_solver.cpp log.cpp + naming.cpp op_constraint.cpp polysat_ast.cpp restart.cpp @@ -20,6 +21,7 @@ z3_add_component(polysat search_state.cpp simplify.cpp simplify_clause.cpp + slicing.cpp smul_fl_constraint.cpp solver.cpp superposition.cpp diff --git a/src/math/polysat/naming.cpp b/src/math/polysat/naming.cpp new file mode 100644 index 000000000..8a3d2449e --- /dev/null +++ b/src/math/polysat/naming.cpp @@ -0,0 +1,65 @@ +/*++ +Copyright (c) 2023 Microsoft Corporation + +Module Name: + + polysat definitions + +Author: + + Jakob Rath 2023-06-01 + +--*/ + +#include "math/polysat/naming.h" +#include "math/polysat/solver.h" +#include "math/polysat/log.h" + +namespace polysat { + + void name_manager::push_var(pdd pv) { + SASSERT(pv.is_var()); + SASSERT_EQ(pv.var(), m_terms.size()); + pvar const v = pv.var(); + m_terms.push_back(std::move(pv)); + SASSERT(!is_name(v)); + } + + void name_manager::pop_var() { + pvar const v = m_terms.size() - 1; + if (is_name(v)) { + name_key key{m_terms[v]}; + m_names.remove(key); + } + m_terms.pop_back(); + } + + void name_manager::set_name(pvar v, pdd const& t) { + SASSERT(!is_name(v)); + name_key key{t}; + SASSERT(!m_names.contains(key)); + m_names.insert(key, v); + m_terms[v] = t; + } + + pvar name_manager::get_name(pdd const& t) const { + name_key key{t}; + auto it = m_names.find_iterator(key); + if (it == m_names.end()) + return null_var; + return it->m_value; + } + + pvar name_manager::mk_name(pdd const& t) { + if (t.is_var()) + return t.var(); + pvar v = get_name(t); + if (v != null_var) + return v; + v = s.add_var(t.power_of_2()); + s.add_eq(s.var(v), t); + set_name(v, t); + return v; + } + +} diff --git a/src/math/polysat/naming.h b/src/math/polysat/naming.h new file mode 100644 index 000000000..35cc4c38f --- /dev/null +++ b/src/math/polysat/naming.h @@ -0,0 +1,65 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + polysat definitions (define variables as names for terms) + +Author: + + Jakob Rath 2023-06-01 + +--*/ +#pragma once +#include "math/polysat/types.h" +#include + +namespace polysat { + + class solver; + + class name_manager final { + + struct name_key { + // NOTE: this is only optional because table2map requires a default constructor + std::optional term; + + name_key() = default; + name_key(pdd term): term(std::move(term)) {} + + bool operator==(name_key const& other) const { + return term == other.term; + } + + unsigned hash() const { + return term ? term->hash() : 0; + } + }; + using name_hash = obj_hash; + using name_eq = default_eq; + using name_map = map; + + solver& s; + name_map m_names; // term -> name + vector m_terms; // name -> term + + void set_name(pvar v, pdd const& term); + + public: + name_manager(solver& s): s(s) {} + + void push_var(pdd v); + void pop_var(); + + /** Whether v is a definition for a term */ + bool is_name(pvar v) const { return !m_terms[v].is_var() || m_terms[v].var() != v; } + + /** Return name for term, or null_var if none has been created yet */ + pvar get_name(pdd const& term) const; + bool has_name(pdd const& term) const { return get_name(term) != null_var; } + + /** Return name for term, creating one if necessary */ + pvar mk_name(pdd const& term); + }; + +} diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp new file mode 100644 index 000000000..1e3ab7135 --- /dev/null +++ b/src/math/polysat/slicing.cpp @@ -0,0 +1,225 @@ +/*++ +Copyright (c) 2023 Microsoft Corporation + +Module Name: + + polysat slicing + +Author: + + Jakob Rath 2023-06-01 + +--*/ + +#include "math/polysat/slicing.h" +#include "math/polysat/solver.h" +#include "math/polysat/log.h" + +namespace polysat { + + void slicing::push_var() { + m_stack.push_scope(); // TODO: we don't need a scope for each variable +#if 0 + m_src.push_back(null_var); + m_hi.push_back(0); + m_lo.push_back(0); +#endif + pvar const v = m_var_slices.size(); + slice_idx const s = alloc_slice(); + m_var_slices.push_back(s); + } + + void slicing::pop_var() { +#if 0 + if (m_src != null_var) { + extract_key key{m_src.back(), m_hi.back(), m_lo.back()}; + m_extracted.remove(key); + } + m_src.pop_back(); + m_hi.pop_back(); + m_lo.pop_back(); +#endif + m_var_slices.pop_back(); + m_stack.pop_scope(1); + } + + slicing::slice_idx slicing::alloc_slice() { + slice_idx const s = m_slices_uf.mk_var(); + SASSERT_EQ(s, m_slices.size()); + m_slices.push_back({}); + m_stack.push_ptr(&m_alloc_slice_trail); + return s; + } + + void slicing::alloc_slice_trail::undo() { + m_owner.m_slices.pop_back(); + } + + void slicing::set_extract(pvar v, pvar src, unsigned hi, unsigned lo) { +#if 0 + SASSERT(!is_extract(v)); + SASSERT(lo < hi && hi <= s.size(src)); + SASSERT_EQ(hi - lo, s.size(v)); + SASSERT(src < v); + SASSERT(!m_extracted.contains(extract_key{src, hi, lo})); +#if 0 // try without this first + if (is_extract(src)) { + // y = (x[k:m])[h:l] = x[h+m:l+m] + unsigned const offset = m_lo[src]; + set_extract(m_src[src], hi + offset, lo + offset); + return; + } +#endif + m_extracted.insert({src, hi, lo}, v); + m_src[v] = src; + m_hi[v] = hi; + m_lo[v] = lo; +#endif + } + + slicing::slice_info slicing::var2slice(pvar v) const { + slice_info si; + si.idx = m_var_slices[v]; + si.hi = s.size(v) - 1; + si.lo = 0; + return si; + } + + slicing::slice_info slicing::sub_hi(slice_info const& parent) const { + SASSERT(has_sub(parent)); + slice const& parent_slice = m_slices[parent.idx]; + slice_info si; + si.idx = parent_slice.sub; + si.hi = parent.hi; + si.lo = parent_slice.cut + 1; + SASSERT(si.hi >= si.lo); + return si; + } + + slicing::slice_info slicing::sub_lo(slice_info const& parent) const { + SASSERT(has_sub(parent)); + slice const& parent_slice = m_slices[parent.idx]; + slice_info si; + si.idx = parent_slice.sub + 1; + si.hi = parent_slice.cut; + si.lo = parent.lo; + SASSERT(si.hi >= si.lo); + return si; + } + + unsigned slicing::get_cut(slice_info const& si) const { + SASSERT(has_sub(si)); + return m_slices[si.idx].cut; + } + + void slicing::split(slice_info const& si, unsigned const cut) { + SASSERT(!has_sub(si)); + SASSERT(si.hi > cut); SASSERT(cut >= si.lo); + slice_idx const sub1 = alloc_slice(); + slice_idx const sub2 = alloc_slice(); + slice& s = m_slices[si.idx]; + s.cut = cut; + s.sub = sub1; + SASSERT_EQ(sub2, sub1 + 1); + } + + void slicing::mk_slice(slice_info const& src, unsigned const hi, unsigned const lo, vector& out) + { + // extracted range must be fully contained inside the src slice + SASSERT(src.hi >= hi); SASSERT(hi >= lo); SASSERT(lo >= src.lo); + if (src.hi == hi && src.lo == lo) { + out.push_back(src); + return; + } + if (has_sub(src)) { + // src is split into [src.hi, cut+1] and [cut, src.lo] + unsigned const cut = get_cut(src); + if (lo >= cut + 1) + return mk_slice(sub_hi(src), hi, lo, out); + else if (cut >= hi) + return mk_slice(sub_lo(src), hi, lo, out); + else { + SASSERT(hi > cut && cut >= lo); + // desired range spans over the cutpoint, so we get multiple slices in the result + mk_slice(sub_hi(src), hi, cut + 1, out); + mk_slice(sub_lo(src), cut, lo, out); + return; + } + } + else { + // [src.hi, src.lo] has no subdivision yet + if (src.hi > hi) { + split(src, hi); + mk_slice(sub_lo(src), hi, lo, out); + return; + } + else { + SASSERT(src.hi == hi); + SASSERT(lo > src.lo); + split(src, lo - 1); + slice_info si = sub_hi(src); + SASSERT_EQ(si.hi, hi); SASSERT_EQ(si.lo, lo); + out.push_back(si); + return; + } + } + UNREACHABLE(); + } + + pvar slicing::mk_extract_var(pvar src, unsigned hi, unsigned lo) { + vector slices; + mk_slice(var2slice(src), hi, lo, slices); + // src[hi:lo] is the concatenation of the returned slices + // TODO: for each slice, set_extract + +#if 0 + extract_key key{src, hi, lo}; + auto it = m_extracted.find_iterator(key); + if (it != m_extracted.end()) + return it->m_value; + pvar v = s.add_var(hi - lo); + set_extract(v, src, hi, lo); + return v; +#endif + } + + pdd slicing::mk_extract(pvar src, unsigned hi, unsigned lo) { + return s.var(mk_extract_var(src, hi, lo)); + } + + pdd slicing::mk_extract(pdd const& p, unsigned hi, unsigned lo) { + if (!lo) { + // TODO: we could push the extract down into variables of the term instead of introducing a name. + } + pvar const v = s.m_names.mk_name(p); + return mk_extract(v, hi, lo); + } + + pdd slicing::mk_concat(pdd const& p, pdd const& q) { +#if 0 + // v := p ++ q (new variable of size |p| + |q|) + // v[:|q|] = p + // v[|q|:] = q + unsigned const p_sz = p.power_of_2(); + unsigned const q_sz = q.power_of_2(); + unsigned const v_sz = p_sz + q_sz; + // TODO: lookup to see if we can reuse a variable + // either: + // - table of concats + // - check for variable with v[:|q|] = p and v[|q|:] = q in extract table (probably better) + pvar const v = s.add_var(v_sz); + + // TODO: probably wrong to use names for p, q. + // we should rather check if there's already an extraction for v[...] and reuse that variable. + pvar const p_name = s.m_names.mk_name(p); + pvar const q_name = s.m_names.mk_name(q); + set_extract(p_name, v, v_sz, q_sz); + set_extract(q_name, v, q_sz, 0); +#endif + NOT_IMPLEMENTED_YET(); + } + + void slicing::propagate(pvar v) { + } + +} diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h new file mode 100644 index 000000000..5e6bd24ea --- /dev/null +++ b/src/math/polysat/slicing.h @@ -0,0 +1,154 @@ +/*++ +Copyright (c) 2023 Microsoft Corporation + +Module Name: + + polysat slicing (relating variables of different bit-widths by extraction) + +Author: + + Jakob Rath 2023-06-01 + +Notation: + + Let x be a bit-vector of width w. + Let l, h indices such that 0 <= l <= h < w. + Then x[h:l] extracts h - l + 1 bits of x. + Shorthands: + - x[h:] stands for x[h:0], and + - x[:l] stands for x[w-1:l]. + + Example: + 0001[0:] = 1 + 0001[2:0] = 001 + +--*/ +#pragma once +#include "math/polysat/types.h" +#include "util/trail.h" +#include "util/union_find.h" + +namespace polysat { + + class solver; + + class slicing final { + + solver& s; + + /// If y := x[h:l], then m_src[y] = x, m_hi[y] = h, m_lo[y] = l. + /// Otherwise m_src[y] = null_var. + /// + /// Invariants: + /// m_src[y] != null_var ==> m_src[y] < y (at least as long as we always introduce new variables for extract terms.) + /// m_lo[y] <= m_hi[y] + unsigned_vector m_src; + unsigned_vector m_hi; + unsigned_vector m_lo; + +#if 0 + struct extract_key { + pvar src; + unsigned hi; + unsigned lo; + + bool operator==(extract_key const& other) const { + return src == other.src && hi == other.hi && lo == other.lo; + } + + unsigned hash() const { + return mk_mix(src, hi, lo); + } + }; + using extract_hash = obj_hash; + using extract_eq = default_eq; + using extract_map = map; + + extract_map m_extracted; ///< src, hi, lo -> v + // need src -> [v] and v -> [src] for propagation? +#endif + + + + + trail_stack m_stack; + + using slice_idx = unsigned; + static constexpr slice_idx null_slice_idx = UINT_MAX; + + struct slice { + // If sub != null_slice_idx, the bit-vector x has been sliced into x[|x|-1:cut+1] and x[cut:0] + unsigned cut = UINT_MAX; + // If sub != null_slice_idx, the sub-slices are at indices sub and sub+1 + slice_idx sub = null_slice_idx; + + bool has_sub() const { return cut != 0; } + slice_idx sub_hi() const { return sub; } + slice_idx sub_lo() const { return sub + 1; } + }; + svector m_slices; // slice_idx -> slice + svector m_var_slices; // pvar -> slice_idx + + // union_find over slices (union_find vars are indices into m_slices, i.e., slice_idx) + union_find m_slices_uf; + + slice_idx alloc_slice(); + + friend class alloc_slice_trail; + class alloc_slice_trail : public trail { + slicing& m_owner; + public: + alloc_slice_trail(slicing& o): m_owner(o) {} + void undo() override; + }; + alloc_slice_trail m_alloc_slice_trail; + + void set_extract(pvar v, pvar src, unsigned hi_bit, unsigned lo_bit); + + struct slice_info { + slice_idx idx; + unsigned hi; + unsigned lo; + }; + slice_info var2slice(pvar v) const; + bool has_sub(slice_info const& si) const { return m_slices[si.idx].has_sub(); } + slice_info sub_hi(slice_info const& si) const; + slice_info sub_lo(slice_info const& si) const; + unsigned get_cut(slice_info const& si) const; + void split(slice_info const& si, unsigned cut); + void mk_slice(slice_info const& src, unsigned hi, unsigned lo, vector& out); + + public: + slicing(solver& s): + s(s), + m_slices_uf(*this), + m_alloc_slice_trail(*this) + {} + + trail_stack& get_trail_stack() { return m_stack; } + + void push_var(); + void pop_var(); + + bool is_extract(pvar v) const { return m_src[v] != null_var; } + + /** Get variable representing x[hi:lo] */ + pvar mk_extract_var(pvar x, unsigned hi, unsigned lo); + + /** Create expression for x[hi:lo] */ + pdd mk_extract(pvar x, unsigned hi, unsigned lo); + + /** Create expression for p[hi:lo] */ + pdd mk_extract(pdd const& p, unsigned hi, unsigned lo); + + /** Create expression for p ++ q */ + pdd mk_concat(pdd const& p, pdd const& q); + + // propagate: + // - value assignments + // - fixed bits + // - intervals ????? -- that will also need changes in the viable algorithm + void propagate(pvar v); + }; + +} diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index e9cf339a3..42c6a843a 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -41,6 +41,8 @@ namespace polysat { m_bvars(*this), m_free_pvars(m_activity), m_constraints(*this), + m_names(*this), + m_slicing(*this), m_search(*this) { } @@ -134,7 +136,7 @@ namespace polysat { } unsigned solver::add_var(unsigned sz) { - pvar v = m_value.size(); + pvar const v = m_value.size(); m_value.push_back(rational::zero()); m_justification.push_back(justification::unassigned()); m_viable.push_var(sz); @@ -145,6 +147,7 @@ namespace polysat { m_size.push_back(sz); m_trail.push_back(trail_instr_t::add_var_i); m_free_pvars.mk_var_eh(v); + m_names.push_var(var(v)); // needs m_vars return v; } @@ -165,6 +168,7 @@ namespace polysat { m_vars.pop_back(); m_size.pop_back(); m_free_pvars.del_var_eh(v); + m_names.pop_var(); } void solver::assign_eh(signed_constraint c, dependency dep) { diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 8fa3c5c6e..d46c87261 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -24,8 +24,10 @@ Author: #include "math/polysat/constraint.h" #include "math/polysat/constraint_manager.h" #include "math/polysat/clause_builder.h" +#include "math/polysat/naming.h" #include "math/polysat/simplify_clause.h" #include "math/polysat/simplify.h" +#include "math/polysat/slicing.h" #include "math/polysat/restart.h" #include "math/polysat/ule_constraint.h" #include "math/polysat/justification.h" @@ -118,6 +120,7 @@ namespace polysat { friend class conflict_explainer; friend class simplify_clause; friend class simplify; + friend class slicing; friend class restart; friend class explainer; friend class inference_engine; @@ -136,6 +139,7 @@ namespace polysat { friend class saturation; friend class parity_tracker; friend class constraint_manager; + friend class name_manager; friend class scoped_solverv; friend class test_polysat; friend class test_fi; @@ -160,6 +164,8 @@ namespace polysat { config m_config; // Per constraint state constraint_manager m_constraints; + name_manager m_names; + slicing m_slicing; // Per variable information vector m_value; // assigned value @@ -313,6 +319,9 @@ namespace polysat { void push_reinit_stack(clause& c); + /** Get variable representing v[hi:lo] */ + pvar extract_var(pvar v, unsigned hi, unsigned lo); + void add_clause(clause_ref clause); void add_clause(clause& clause); void add_clause(signed_constraint c1, bool is_redundant); @@ -405,6 +414,12 @@ namespace polysat { */ pdd var(pvar v) { return m_vars[v]; } + /** Create expression for v[hi:lo] */ + pdd extract(pvar v, unsigned hi, unsigned lo); + + /** Create expression for p[hi:lo] */ + pdd extract(pdd const& p, unsigned hi, unsigned lo); + /** * Create terms for unsigned quot-rem *