mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

relevant level should be based on what's to appear in the lemma

Browse source
This commit is contained in:
Jakob Rath 2024-03-21 11:05:55 +01:00
parent 7d1a57b6e9
commit acd05686e4
2 changed files with 32 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/sat/smt/polysat/project_interval.cpp
View file

@ -74,18 +74,23 @@ namespace polysat {
} }
} }
dependency project_interval::dep_target(fixed_slice const& target) { dependency project_interval::dep_target_sub(fixed_slice const& target) {
SASSERT(target.child != null_var); SASSERT(target.child != null_var);
SASSERT(target.length == c.size(target.child)); SASSERT(target.length == c.size(target.child));
return dep_target(target.child, target.value); return dep_target_sub(target.child, target.offset);
} }
dependency project_interval::dep_target(pvar w, rational const& value) { dependency project_interval::dep_target_sub(pvar w, unsigned w_off) {
SASSERT(w != null_var);
return offset_claim{m_var, offset_slice{w, w_off}};
}
dependency project_interval::dep_target_fixed(pvar w, rational const& value) {
SASSERT(w != null_var); SASSERT(w != null_var);
return fixed_claim(w, null_var, value, 0, c.size(w)); return fixed_claim(w, null_var, value, 0, c.size(w));
} }
void project_interval::ensure_target_levels() { void project_interval::ensure_target_levels(unsigned ext_level) {
if (!m_target_levels.empty()) { if (!m_target_levels.empty()) {
SASSERT_EQ(m_target_levels.size(), m_fixed.size()); SASSERT_EQ(m_target_levels.size(), m_fixed.size());
return; return;
@ -94,8 +99,8 @@ namespace polysat {
auto compute_target_level = [&](fixed_slice const& f) -> unsigned { auto compute_target_level = [&](fixed_slice const& f) -> unsigned {
if (f.child == null_var) if (f.child == null_var)
return UINT_MAX; return UINT_MAX;
dependency dep = dep_target(f); dependency dep = dep_target_sub(f);
unsigned level = c.level(dep); unsigned level = std::max(c.level(dep), ext_level);
IF_VERBOSE(4, verbose_stream() << "dep_target " << dep << " at level " << level << "\n"); IF_VERBOSE(4, verbose_stream() << "dep_target " << dep << " at level " << level << "\n");
return level; return level;
}; };
@ -144,7 +149,14 @@ namespace polysat {
} }
void project_interval::select_targets() { void project_interval::select_targets() {
ensure_target_levels();
// compute level of external dependencies (i.e., of m_var \not\in m_interval)
SASSERT(m_deps.size() == m_deps_initial_size);
unsigned ext_level = 0;
for (dependency const& d : m_deps)
ext_level = std::max(ext_level, c.level(d));
ensure_target_levels(ext_level);
m_targets.reset(); m_targets.reset();
unsigned i = 0; unsigned i = 0;
@ -239,8 +251,8 @@ namespace polysat {
// - external explanation for the interval on m_var // - external explanation for the interval on m_var
// - explanation for the fixed parts that were used for projection // - explanation for the fixed parts that were used for projection
// add explanation for m_var[...] = w // add explanation for m_var[...] ~ w
m_deps.push_back(offset_claim{m_var, offset_slice{w, w_off}}); m_deps.push_back(dep_target_sub(w, w_off));
SASSERT(m_result == l_undef); SASSERT(m_result == l_undef);
SASSERT(m_explain.empty()); SASSERT(m_explain.empty());
@ -263,7 +275,7 @@ namespace polysat {
dependency d = c.propagate(sc, m_deps, "propagate from containing slice"); dependency d = c.propagate(sc, m_deps, "propagate from containing slice");
m_explain.push_back(d); m_explain.push_back(d);
m_explain.push_back(dep_target(w, value)); m_explain.push_back(dep_target_fixed(w, value)); // w ~ value
IF_VERBOSE(3, { IF_VERBOSE(3, {
verbose_stream() << "=> v" << w << "[" << y_sz << "] not in " << ivl << "\n"; verbose_stream() << "=> v" << w << "[" << y_sz << "] not in " << ivl << "\n";

14
src/sat/smt/polysat/project_interval.h
View file

@ -34,9 +34,9 @@ namespace polysat {
/* fixed subslices of source variable */ /* fixed subslices of source variable */
fixed_bits_vector m_fixed; fixed_bits_vector m_fixed;
unsigned_vector m_fixed_levels; // cache for level(dep_fixed(m_fixed[i])) unsigned_vector m_fixed_levels; // cache for level(dep_fixed(m_fixed[i]))
unsigned_vector m_target_levels; // cache for level(dep_target(m_fixed[i])) unsigned_vector m_target_levels; // cache for max(level(dep_target_sub(m_fixed[i])), level(m_deps))
void ensure_fixed_levels(); void ensure_fixed_levels();
void ensure_target_levels(); void ensure_target_levels(unsigned ext_level);
// target slices for which we will try projection. // target slices for which we will try projection.
// - first entry is target with lowest level (more generic: possibly smaller interval, but less dependencies) // - first entry is target with lowest level (more generic: possibly smaller interval, but less dependencies)
@ -62,8 +62,14 @@ namespace polysat {
* target pvar is fixed * target pvar is fixed
* w ~ value * w ~ value
*/ */
dependency dep_target(fixed_slice const& target); dependency dep_target_fixed(pvar w, rational const& value);
dependency dep_target(pvar w, rational const& value);
/**
* target pvar is subslice of m_var
* m_var[...] ~ w
*/
dependency dep_target_sub(fixed_slice const& target);
dependency dep_target_sub(pvar w, unsigned w_off);
/** /**
* Let x = concat(y, z) and x not in [lo;hi[. * Let x = concat(y, z) and x not in [lo;hi[.