extract/concat slicing wip

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

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;
+    }
+
+}

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 <optional>
+
+namespace polysat {
+
+    class solver;
+
+    class name_manager final {
+
+        struct name_key {
+            // NOTE: this is only optional because table2map requires a default constructor
+            std::optional<pdd> 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<name_key>;
+        using name_eq = default_eq<name_key>;
+        using name_map = map<name_key, pvar, name_hash, name_eq>;
+
+        solver&     s;
+        name_map    m_names;    // term -> name
+        vector<pdd> 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);
+    };
+
+}

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<slice_info>& 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<slice_info> 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) {
+    }
+
+}

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<extract_key>;
+        using extract_eq = default_eq<extract_key>;
+        using extract_map = map<extract_key, pvar, extract_hash, extract_eq>;
+
+        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<slice>      m_slices;       // slice_idx -> slice
+        svector<slice_idx>  m_var_slices;   // pvar -> slice_idx
+
+        // union_find over slices (union_find vars are indices into m_slices, i.e., slice_idx)
+        union_find<slicing> 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<slice_info>& 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);
+    };
+
+}

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) {

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<rational>         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
         *