mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-19 01:32:17 +00:00
Code Activity

reuse more slices for extractions

Browse source
This commit is contained in:
Jakob Rath 2023-07-26 09:44:17 +02:00
parent 16188945ab
commit 8f314d4a7f
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -875,7 +875,7 @@ namespace polysat {
pvar slicing::mk_extract(enode* src, unsigned hi, unsigned lo, pvar replay_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, false); // TODO: we don't need a base if we can reuse some intermediary slice, do we?
pvar v = null_var; pvar v = null_var;
// try to re-use variable of an existing slice // try to re-use variable of an existing slice
if (slices.size() == 1) if (slices.size() == 1)
@ -892,7 +892,7 @@ namespace polysat {
// allocate new variable if we cannot reuse it // allocate new variable if we cannot reuse it
if (v == null_var) if (v == null_var)
v = m_solver.add_var(hi - lo + 1); v = m_solver.add_var(hi - lo + 1);
#if 0 #if 1
// slice didn't have a variable yet; so we can re-use it for the new variable // slice didn't have a variable yet; so we can re-use it for the new variable
// (we end up with a "phantom" enode that was first created for the variable) // (we end up with a "phantom" enode that was first created for the variable)
if (slices.size() == 1) { if (slices.size() == 1) {