mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

make concat work with value args

Browse source
This commit is contained in:
Jakob Rath 2023-07-24 10:25:44 +02:00
parent e45fed472d
commit b51c634294
4 changed files with 23 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/dd/dd_pdd.h
View file

@ -263,6 +263,7 @@ namespace dd {
inline PDD lo(PDD p) const { return m_nodes[p].m_lo; }
inline PDD hi(PDD p) const { return m_nodes[p].m_hi; }
inline rational const& val(PDD p) const { SASSERT(is_val(p)); return m_values[lo(p)]; }
inline rational const& val_signed(PDD p) const { SASSERT(m_semantics == mod2_e || m_semantics == mod2N_e); rational const& a = val(p); return a.get_bit(power_of_2() - 1) ? a - two_to_N() : a; }
inline void inc_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount++; SASSERT(!m_free_nodes.contains(p)); }
inline void dec_ref(PDD p) { if (m_nodes[p].m_refcount != max_rc) m_nodes[p].m_refcount--; SASSERT(!m_free_nodes.contains(p)); }
inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; }
@ -421,7 +422,8 @@ namespace dd {
pdd hi() const { return pdd(m->hi(root), m); }
unsigned index() const { return root; }
unsigned var() const { return m->var(root); }
rational const& val() const { SASSERT(is_val()); return m->val(root); }
rational const& val() const { return m->val(root); }
rational const& val_signed() const { return m->val_signed(root); }
rational const& leading_coefficient() const;
rational const& offset() const { return m->offset(root); }
bool is_val() const { return m->is_val(root); }

27
src/math/polysat/constraint_manager.cpp
View file

@ -614,28 +614,23 @@ namespace polysat {
unsigned const p_sz = p.power_of_2();
unsigned const q_sz = q.power_of_2();
unsigned const v_sz = p_sz + q_sz;
if (p.is_val() && q.is_val()) {
rational const val = p.val() * rational::power_of_two(q_sz) + q.val();
return s.sz2pdd(v_sz).mk_val(val);
}
if (p.is_val()) {
// TODO
}
if (q.is_val()) {
// TODO
}
auto const args = {p, q};
return concat(args.size(), args.begin());
if (p.is_val() || q.is_val())
return zero_ext(p, q_sz) * rational::power_of_two(q_sz) + zero_ext(q, p_sz);
auto const args = {s.m_names.mk_name(p), s.m_names.mk_name(q)};
pvar const v = s.m_slicing.mk_concat(args.size(), args.begin());
return s.var(v);
}
pdd constraint_manager::concat(unsigned num_args, pdd const* args) {
SASSERT(num_args > 0);
if (num_args == 1)
return args[0];
if (num_args == 2)
return concat(args[0], args[1]);
// TODO: special cases when args are values?
pvar_vector pvar_args;
for (unsigned i = 0; i < num_args; ++i)
pvar_args.push_back(s.m_names.mk_name(args[i]));
pvar_args.push_back(s.m_names.mk_name_even_if_value(args[i]));
pvar const v = s.m_slicing.mk_concat(num_args, pvar_args.data());
return s.var(v);
}
@ -644,6 +639,8 @@ namespace polysat {
SASSERT(extra_bits > 0);
unsigned const p_sz = p.power_of_2();
unsigned const v_sz = p_sz + extra_bits;
if (p.is_val())
return s.sz2pdd(v_sz).mk_val(p.val());
pdd const q = s.var(s.m_names.mk_name(p));
constraint_dedup::bv_ext_args const args = {false, q.var(), extra_bits};
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
@ -660,8 +657,10 @@ namespace polysat {
pdd constraint_manager::sign_ext(pdd const& p, unsigned extra_bits) {
SASSERT(extra_bits > 0);
unsigned const p_sz = p. power_of_2();
unsigned const p_sz = p.power_of_2();
unsigned const v_sz = p_sz + extra_bits;
if (p.is_val())
return s.sz2pdd(v_sz).mk_val(p.val_signed());
pdd const q = s.var(s.m_names.mk_name(p));
constraint_dedup::bv_ext_args const args = {true, q.var(), extra_bits};
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);

4
src/math/polysat/naming.cpp
View file

@ -52,10 +52,10 @@ namespace polysat {
return it->m_value;
}
pvar name_manager::mk_name(pdd const& t) {
pvar name_manager::mk_name(pdd const& t, bool allow_values) {
if (t.is_var())
return t.var();
SASSERT(!t.is_val()); // we probably don't want names for constants
SASSERT(allow_values || !t.is_val()); // we probably don't want names for constants
pvar v = get_name(t);
if (v != null_var)
return v;

6
src/math/polysat/naming.h
View file

@ -45,6 +45,8 @@ namespace polysat {
void set_name(pvar v, pdd const& term);
pvar mk_name(pdd const& term, bool allow_values);
public:
name_manager(solver& s): s(s) {}
@ -53,13 +55,15 @@ namespace polysat {
/** 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; }
pdd const& get_definition(pvar v) const { SASSERT(is_name(v)); return m_terms[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);
pvar mk_name(pdd const& term) { return mk_name(term, false); }
pvar mk_name_even_if_value(pdd const& term) { return mk_name(term, true); }
};
}