mk_value_slice

src/math/polysat/slicing.cpp

@@ -68,6 +68,7 @@ Recycle the z3 egraph?
 */
 
 
+#include "ast/reg_decl_plugins.h"
 #include "math/polysat/slicing.h"
 #include "math/polysat/solver.h"
 #include "math/polysat/log.h"
@@ -96,6 +97,9 @@ namespace polysat {
         m_concat_decls(m_ast),
         m_egraph(m_ast)
     {
+        reg_decl_plugins(m_ast);
+        // m_ast.register_plugin(symbol("bv"), alloc(bv_decl_plugin));
+        m_bv = alloc(bv_util, m_ast);
         m_slice_sort = m_ast.mk_uninterpreted_sort(symbol("slice"));
         m_egraph.set_display_justification(display_dep);
     }
@@ -140,10 +144,7 @@ namespace polysat {
         while (m_trail.size() > target_size) {
             switch (m_trail.back()) {
             case trail_item::add_var:           undo_add_var();         break;
-            case trail_item::alloc_slice:       undo_alloc_slice();     break;
             case trail_item::split_core:        undo_split_core();      break;
-            // case trail_item::merge_base:        undo_merge_base();      break;
-            // case trail_item::mk_value_slice:    undo_mk_value_slice();  break;
             default: UNREACHABLE();
             }
             m_trail.pop_back();
@@ -153,8 +154,7 @@ namespace polysat {
 
     void slicing::add_var(unsigned bit_width) {
         pvar const v = m_var2slice.size();
-        enode* s = alloc_slice(bit_width);
+        enode* s = alloc_slice(bit_width, v);
-        info(s).var = v;
         m_var2slice.push_back(s);
     }
 
@@ -162,19 +162,31 @@ namespace polysat {
         m_var2slice.pop_back();
     }
 
-    slicing::enode* slicing::alloc_slice(unsigned width) {
+    slicing::enode* slicing::alloc_enode(expr* e, unsigned width, pvar var) {
         SASSERT(width > 0);
-        app* a = m_ast.mk_fresh_const("s", m_slice_sort, false);
+        SASSERT(!m_egraph.find(e));
-        euf::enode* n = m_egraph.mk(a, 0, 0, nullptr);  // NOTE: the egraph keeps a strong reference to "a"
+        euf::enode* n = m_egraph.mk(e, 0, 0, nullptr);  // NOTE: the egraph keeps a strong reference to 'e'
         m_info.reserve(n->get_id() + 1);
         slice_info& i = info(n);
         i.reset();
         i.width = width;
-        m_trail.push_back(trail_item::alloc_slice);
+        i.var = var;
         return n;
     }
 
-    void slicing::undo_alloc_slice() {
+    slicing::enode* slicing::find_or_alloc_enode(expr* e, unsigned width, pvar var) {
+        enode* n = m_egraph.find(e);
+        if (n) {
+            SASSERT_EQ(info(n).width, width);
+            SASSERT_EQ(info(n).var, var);
+            return n;
+        }
+        return alloc_enode(e, width, var);
+    }
+
+    slicing::enode* slicing::alloc_slice(unsigned width, pvar var) {
+        app* a = m_ast.mk_fresh_const("s", m_slice_sort, false);
+        return alloc_enode(a, width, var);
     }
 
     // split a single slice without updating any equivalences
@@ -226,28 +238,24 @@ namespace polysat {
         m_egraph.propagate();  // TODO: could do this later
     }
 
-#if 0
+    slicing::enode* slicing::mk_value_slice(rational const& val, unsigned bit_width) {
-    slicing::slice slicing::mk_value_slice(rational const& val, unsigned bit_width) {
         SASSERT(0 <= val && val < rational::power_of_two(bit_width));
-        val2slice_key key(val, bit_width);
+        app* a = m_bv->mk_numeral(val, bit_width);
-        auto it = m_val2slice.find_iterator(key);
+        enode* s = find_or_alloc_enode(a, bit_width, null_var);
-        if (it != m_val2slice.end())
+        SASSERT(s->interpreted());
-            return it->m_value;
-        slice s = alloc_slice();
-        m_slice_width[s] = bit_width;
-        m_slice2val[s] = val;
-        // m_value_root[s] = s;
-        m_val2slice.insert(key, s);
-        m_val2slice_trail.push_back(std::move(key));
-        m_trail.push_back(trail_item::mk_value_slice);
         return s;
     }
 
-    void slicing::undo_mk_value_slice() {
+    rational slicing::get_value(enode* s) const {
-        m_val2slice.remove(m_val2slice_trail.back());
+        SASSERT(s->interpreted());
-        m_val2slice_trail.pop_back();
+        rational val;
+        VERIFY(try_get_value(s, val));
+        return val;
+    }
+
+    bool slicing::try_get_value(enode* s, rational& val) const {
+        return m_bv->is_numeral(s->get_expr(), val);
     }
-#endif
 
     bool slicing::merge_base(enode* s1, enode* s2, dep_t dep) {
         SASSERT_EQ(width(s1), width(s2));

src/math/polysat/slicing.h

@@ -25,6 +25,7 @@ Notation:
 --*/
 #pragma once
 #include "ast/euf/euf_egraph.h"
+#include "ast/bv_decl_plugin.h"
 #include "math/polysat/types.h"
 #include "math/polysat/constraint.h"
 #include <optional>
@@ -48,6 +49,8 @@ namespace polysat {
 
         struct slice_info {
             unsigned    width   = 0;            // number of bits in the slice
+            // Cut point: if not null_cut, the slice s has been subdivided into s[|s|-1:cut+1] and s[cut:0].
+            // The cut point is relative to the parent slice (rather than a root variable, which might not be unique)
             unsigned    cut     = null_cut;     // cut point, or null_cut if no subslices
             pvar        var     = null_var;     // slice is equivalent to this variable, if any (without dependencies)
             enode*      slice   = nullptr;      // if enode corresponds to a concat(...) expression, this field links to the represented slice.
@@ -65,6 +68,7 @@ namespace polysat {
         solver&                 m_solver;
 
         ast_manager             m_ast;
+        scoped_ptr<bv_util>     m_bv;
         sort_ref                m_slice_sort;
         func_decl_ref_vector    m_concat_decls;
 
@@ -82,41 +86,12 @@ namespace polysat {
         static dep_t decode_dep(void* d);
         static void display_dep(std::ostream& out, void* d);
 
-/*
-        struct val2slice_key {
-            rational value;
-            unsigned bit_width;
-
-            val2slice_key() {}
-            val2slice_key(rational value, unsigned bit_width): value(std::move(value)), bit_width(bit_width) {}
-
-            bool operator==(val2slice_key const& other) const {
-                return bit_width == other.bit_width && value == other.value;
-            }
-
-            unsigned hash() const {
-                return combine_hash(value.hash(), bit_width);
-            }
-        };
-        using val2slice_hash = obj_hash<val2slice_key>;
-        using val2slice_eq = default_eq<val2slice_key>;
-        using val2slice_map = map<val2slice_key, slice, val2slice_hash, val2slice_eq>;
-*/
-
-/*
-        unsigned_vector m_slice_width;  // number of bits in the slice
-        // Cut point: if slice represents bit-vector x, then x has been sliced into x[|x|-1:cut+1] and x[cut:0].
-        // The cut point is relative to the parent slice (rather than a root variable, which might not be unique)
-        // (null_cut for leaf slices)
-        unsigned_vector m_slice_cut;
-        // The sub-slices are at indices sub and sub+1 (or null_slice if there is no subdivision)
-        slice_vector    m_slice_sub;
-*/
-
         slice_info& info(euf::enode* n);
         slice_info const& info(euf::enode* n) const;
 
-        enode* alloc_slice(unsigned width);
+        enode* alloc_enode(expr* e, unsigned width, pvar var);
+        enode* find_or_alloc_enode(expr* e, unsigned width, pvar var);
+        enode* alloc_slice(unsigned width, pvar var = null_var);
 
         enode* var2slice(pvar v) const { return m_var2slice[v]; }
         pvar slice2var(enode* s) const { return info(s).var; }
@@ -131,16 +106,13 @@ namespace polysat {
         /// Lower subslice (direct child, not necessarily the representative)
         enode* sub_lo(enode* s) const { return info(s).sub_lo; }
 
-        // slice val2slice(rational const& val, unsigned bit_width) const;
-
         // Retrieve (or create) a slice representing the given value.
-        // slice mk_value_slice(rational const& val, unsigned bit_width);
+        enode* mk_value_slice(rational const& val, unsigned bit_width);
 
-        // bool has_value(slice s) const { SASSERT_EQ(s, find(s)); return m_slice2val[s].is_nonneg(); }
+        bool has_value(enode* s) const { return s->interpreted(); }
-        // rational const& get_value(slice s) const { SASSERT(has_value(s)); return m_slice2val[s]; }
 
-        // reverse all edges on the path from s to the root of its tree in the proof forest
+        rational get_value(enode* s) const;
-        // void make_proof_root(slice s);
+        bool try_get_value(enode* s, rational& val) const;
 
         /// Split slice s into s[|s|-1:cut+1] and s[cut:0]
         void split(enode* s, unsigned cut);
@@ -196,20 +168,14 @@ namespace polysat {
 
         enum class trail_item {
             add_var,
-            alloc_slice,
             split_core,
-            merge_base,
-            mk_value_slice,
         };
         svector<trail_item> m_trail;
         enode_vector        m_split_trail;
-        // vector<val2slice_key>               m_val2slice_trail;
         unsigned_vector     m_scopes;
 
         void undo_add_var();
-        void undo_alloc_slice();
         void undo_split_core();
-        void undo_mk_value_slice();
 
         mutable enode_vector m_tmp1;
         mutable enode_vector m_tmp2;