mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

fixes

Browse source
This commit is contained in:
Jakob Rath 2023-07-26 09:09:23 +02:00
parent a75daf8681
commit 1e5255508c
2 changed files with 13 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -263,7 +263,7 @@ namespace dd {
inline PDD lo(PDD p) const { return m_nodes[p].m_lo; } 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 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(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 rational get_signed_val(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 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 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]]; } inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; }
@ -423,7 +423,7 @@ namespace dd {
unsigned index() const { return root; } unsigned index() const { return root; }
unsigned var() const { return m->var(root); } unsigned var() const { return m->var(root); }
rational const& val() const { return m->val(root); } rational const& val() const { return m->val(root); }
rational const& val_signed() const { return m->val_signed(root); } rational get_signed_val() const { return m->get_signed_val(root); }
rational const& leading_coefficient() const; rational const& leading_coefficient() const;
rational const& offset() const { return m->offset(root); } rational const& offset() const { return m->offset(root); }
bool is_val() const { return m->is_val(root); } bool is_val() const { return m->is_val(root); }

18
src/math/polysat/slicing.cpp
View file

@ -198,11 +198,12 @@ namespace polysat {
case trail_item::split_core: case trail_item::split_core:
undo_split_core(); undo_split_core();
break; break;
case trail_item::mk_extract: case trail_item::mk_extract: {
extract_args const& args = m_extract_trail.back(); extract_args const& args = m_extract_trail.back();
replay_extract.push_back({args, m_extract_dedup[args]}); replay_extract.push_back({args, m_extract_dedup[args]});
undo_mk_extract(); undo_mk_extract();
break; break;
}
case trail_item::mk_concat: case trail_item::mk_concat:
num_replay_concat++; num_replay_concat++;
break; break;
@ -219,22 +220,25 @@ namespace polysat {
unsigned concat_idx = m_concat_trail.size() - num_replay_concat; unsigned concat_idx = m_concat_trail.size() - num_replay_concat;
for (unsigned i = target_size; i < m_trail.size(); ++i) { for (unsigned i = target_size; i < m_trail.size(); ++i) {
switch (m_trail[i]) { switch (m_trail[i]) {
case trail_item::add_var: case trail_item::add_var: {
unsigned const sz = replay_add_var[--add_var_idx]; unsigned const sz = replay_add_var[--add_var_idx];
add_var(replay_add_var[i]); add_var(sz);
break; break;
}
case trail_item::split_core: case trail_item::split_core:
/* do nothing */ /* do nothing */
break; break;
case trail_item::mk_extract: case trail_item::mk_extract: {
auto const [args, v] = replay_extract[--extract_idx]; auto const [args, v] = replay_extract[--extract_idx];
this->replay_extract(args, v); this->replay_extract(args, v);
break; break;
case trail_item::mk_concat: }
auto ci = m_concat_trail[concat_idx++]; case trail_item::mk_concat: {
auto const ci = m_concat_trail[concat_idx++];
num_replay_concat++; num_replay_concat++;
replay_concat(ci.num_args, &m_concat_args[ci.args_idx], ci.v); replay_concat(ci.num_args, &m_concat_args[ci.args_idx], ci.v);
break; break;
}
default: UNREACHABLE(); default: UNREACHABLE();
} }
@ -768,7 +772,7 @@ namespace polysat {
get_base_core<true>(src, out_base); get_base_core<true>(src, out_base);
} }
pvar slicing::mk_extract(enode* src, unsigned hi, unsigned lo, pvar replay_var = null_var) { pvar slicing::mk_extract(enode* src, unsigned hi, unsigned lo, pvar replay_var) {
enode_vector& slices = m_tmp3; enode_vector& slices = m_tmp3;
SASSERT(slices.empty()); SASSERT(slices.empty());
mk_slice(src, hi, lo, slices, false, true); mk_slice(src, hi, lo, slices, false, true);