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

add dependencies from var equivalence

Browse source
This commit is contained in:
Jakob Rath 2023-12-07 15:33:11 +01:00
parent e1aa00352d
commit a6c593b3d3
2 changed files with 29 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/math/polysat/viable.cpp
View file

@ -1883,16 +1883,16 @@ namespace polysat {
// e.g.: v^2 + w^2 == 0; w := 1
// - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v):
// e.g.: v^2 + w^2 == 0; w^2 == 1
uint_set to_explain;
uint_set vars_to_explain;
for (unsigned d : us.unsat_core()) {
auto [x, lit] = deps[d];
if (x != v)
to_explain.insert(x);
vars_to_explain.insert(x);
signed_constraint c = s.lit2cnstr(lit);
core.insert(c);
core.insert_vars(c);
}
for (pvar x : to_explain) {
for (pvar x : vars_to_explain) {
s.m_slicing.explain_simple_overlap(v, x, [this, &core](sat::literal l) {
core.insert(s.lit2cnstr(l));
});
@ -1912,9 +1912,12 @@ namespace polysat {
bool create_lemma = true;
clause_builder lemma(s);
uint_set vars_to_explain;
char const* lemma_name = nullptr;
// if there is a full interval, it should be the only one in the given vector
if (intervals.size() == 1 && intervals[0]->interval.is_full()) {
lemma_name = "viable (full interval)";
entry const* e = intervals[0];
for (auto sc : e->side_cond)
lemma.insert_eval(~sc);
@ -1923,30 +1926,39 @@ namespace polysat {
core.insert(src);
core.insert_vars(src);
}
core.add_lemma("viable (single full interval)", lemma.build());
if (v != e->var)
vars_to_explain.insert(e->var);
}
else {
SASSERT(all_of(intervals, [](entry* e) { return e->interval.is_proper(); }));
lemma_name = "viable (proper intervals)";
// allocate one dummy space in intervals storage to simplify recursive calls
intervals.push_back(nullptr);
entry** intervals_begin = intervals.data() + first_interval;
unsigned num_intervals = intervals.size() - first_interval - 1;
if (!set_conflict_by_interval_rec(v, w, intervals_begin, num_intervals, core, create_lemma, lemma))
if (!set_conflict_by_interval_rec(v, w, intervals_begin, num_intervals, core, create_lemma, lemma, vars_to_explain))
return false;
if (create_lemma)
core.add_lemma("viable", lemma.build());
}
for (pvar x : vars_to_explain) {
s.m_slicing.explain_simple_overlap(v, x, [this, &core, &lemma](sat::literal l) {
lemma.insert(~l);
core.insert(s.lit2cnstr(l));
});
}
if (create_lemma)
core.add_lemma(lemma_name, lemma.build());
core.logger().log(inf_fi(*this, v));
core.init_viable_end(v);
return true;
}
bool viable::set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, conflict& core, bool& create_lemma, clause_builder& lemma) {
bool viable::set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, conflict& core, bool& create_lemma, clause_builder& lemma, uint_set& vars_to_explain) {
SASSERT(std::all_of(intervals, intervals + num_intervals, [w](entry const* e) { return e->bit_width <= w; }));
// TODO: assert invariants on intervals list
rational const& mod_value = rational::power_of_two(w);
@ -2016,7 +2028,7 @@ namespace polysat {
entry* old = intervals[last_idx + 1];
intervals[last_idx + 1] = tmp;
bool result = set_conflict_by_interval_rec(v, w2, &intervals[j], last_idx - j + 2, core, create_lemma, lemma);
bool result = set_conflict_by_interval_rec(v, w2, &intervals[j], last_idx - j + 2, core, create_lemma, lemma, vars_to_explain);
intervals[last_idx + 1] = old;
@ -2070,20 +2082,20 @@ namespace polysat {
j = best_j;
n = intervals[best_j];
if (!update_interval_conflict(v, e->interval.hi(), n, core, create_lemma, lemma))
if (!update_interval_conflict(v, e->interval.hi(), n, core, create_lemma, lemma, vars_to_explain))
return false;
i = j;
e = n;
}
if (!update_interval_conflict(v, e->interval.hi(), longest, core, create_lemma, lemma))
if (!update_interval_conflict(v, e->interval.hi(), longest, core, create_lemma, lemma, vars_to_explain))
return false;
return true;
}
bool viable::update_interval_conflict(pvar v, pdd const& p, entry* n, conflict& core, bool& create_lemma, clause_builder& lemma) {
bool viable::update_interval_conflict(pvar v, pdd const& p, entry* n, conflict& core, bool& create_lemma, clause_builder& lemma, uint_set& vars_to_explain) {
if (!n->valid_for_lemma)
create_lemma = false;
@ -2110,10 +2122,8 @@ namespace polysat {
core.insert_vars(src);
}
if (v != n->var) {
NOT_IMPLEMENTED_YET();
// TODO: s.m_slicing.explain_simple_overlap(v, n->var) [add to both core and lemma]
}
if (v != n->var)
vars_to_explain.insert(n->var);
return true;
}

4
src/math/polysat/viable.h
View file

@ -194,8 +194,8 @@ namespace polysat {
* \pre there are no viable values for v (determined by interval reasoning)
*/
bool set_conflict_by_interval(pvar v, unsigned w, ptr_vector<entry>& intervals, unsigned first_interval);
bool set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, conflict& core, bool& create_lemma, clause_builder& lemma);
bool update_interval_conflict(pvar v, pdd const& p, entry* n, conflict& core, bool& create_lemma, clause_builder& lemma);
bool set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, conflict& core, bool& create_lemma, clause_builder& lemma, uint_set& vars_to_explain);
bool update_interval_conflict(pvar v, pdd const& p, entry* n, conflict& core, bool& create_lemma, clause_builder& lemma, uint_set& vars_to_explain);
/**
* Bitblasting-based query.