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

generalize level

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-15 16:46:30 +01:00
parent 7e7f88ae3d
commit 689c5b4e12
6 changed files with 40 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/conflict_core.cpp
View file

@ -186,11 +186,13 @@ namespace polysat {
auto& premises = it->m_value;
clause_builder c_lemma(s());
for (auto premise : premises) {
LOG_H3("premise: " << premise);
keep(premise);
SASSERT(premise->has_bvar());
SASSERT(premise.bvalue(s()) == l_true); // otherwise the propagation doesn't make sense
SASSERT(premise->has_bvar());
SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true);
// otherwise the propagation doesn't make sense
c_lemma.push(~premise.blit());
active_level = std::max(active_level, s().m_bvars.level(premise.blit()));
active_level = std::max(active_level, premise.level(s()));
}
c_lemma.push(c.blit());
clause* cl = cm().store(c_lemma.build());

12
src/math/polysat/constraint.cpp
View file

@ -219,11 +219,10 @@ namespace polysat {
return *dynamic_cast<ule_constraint const*>(this);
}
std::ostream& constraint::display_extra(std::ostream& out, lbool status) const {
std::ostream& constraint::display_extra(std::ostream& out) const {
out << " (b";
if (has_bvar()) { out << bvar(); } else { out << "_"; }
out << ")";
(void)status;
return out;
}
@ -261,6 +260,15 @@ namespace polysat {
m_unit_clause = cl;
}
unsigned constraint::level(solver& s) const {
if (s.m_bvars.value(sat::literal(bvar())) != l_undef)
return s.m_bvars.level(bvar());
unsigned level = 0;
for (auto v : vars())
level = std::max(level, s.get_level(v));
return level;
}
lbool signed_constraint::bvalue(solver& s) const {
return s.m_bvars.value(blit());
}

5
src/math/polysat/constraint.h
View file

@ -148,7 +148,7 @@ namespace polysat {
constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
protected:
std::ostream& display_extra(std::ostream& out, lbool status) const;
std::ostream& display_extra(std::ostream& out) const;
public:
virtual ~constraint() {}
@ -179,6 +179,7 @@ namespace polysat {
bool contains_var(pvar v) const { return m_vars.contains(v); }
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
sat::bool_var bvar() const { return m_bvar; }
unsigned level(solver& s) const;
clause* unit_clause() const { return m_unit_clause; }
void set_unit_clause(clause* cl);
@ -231,12 +232,14 @@ namespace polysat {
bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); }
bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); }
lbool bvalue(solver& s) const;
unsigned level(solver& s) const { return get()->level(s); }
void narrow(solver& s) { get()->narrow(s, is_positive()); }
inequality as_inequality() const { return get()->as_inequality(is_positive()); }
sat::bool_var bvar() const { return m_constraint->bvar(); }
sat::literal blit() const { return sat::literal(bvar(), is_negative()); }
constraint* get() const { return m_constraint; }
explicit operator bool() const { return !!m_constraint; }
bool operator!() const { return !m_constraint; }

11
src/math/polysat/solver.cpp
View file

@ -744,15 +744,22 @@ namespace polysat {
void solver::add_lemma(clause_ref lemma) {
if (!lemma)
return;
bool non_propagated_literal = false;
LOG("Lemma: " << show_deref(lemma));
for (sat::literal lit : *lemma) {
LOG(" Literal " << lit << " is: " << m_constraints.lookup(lit));
signed_constraint c = m_constraints.lookup(lit);
// Check that fully evaluated constraints are on the stack
SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this));
SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_true(*this));
SASSERT(!c.is_currently_true(*this));
// literals that are added from m_conflict.m_vars have not been assigned.
// they are false in the current model.
if (!m_bvars.is_assigned(lit) && c.is_currently_false(*this)) {
non_propagated_literal = true;
}
// SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this));
// TODO: work out invariant for the lemma. It should be impossible to extend the model in a way that makes the lemma true.
}
// SASSERT(!non_propagated_literal);
SASSERT(lemma->size() > 0);
clause* cl = m_constraints.store(std::move(lemma));
if (cl->size() == 1) {

5
src/math/polysat/ule_constraint.cpp
View file

@ -39,7 +39,7 @@ namespace polysat {
else if (status == l_false) out << " > ";
else out << " <=/> ";
out << m_rhs;
return display_extra(out, status);
return display_extra(out);
}
std::ostream& ule_constraint::display(std::ostream& out) const {
@ -48,7 +48,8 @@ namespace polysat {
out << " == ";
else
out << " <= ";
return out << m_rhs;
out << m_rhs;
return display_extra(out);
}
void ule_constraint::narrow(solver& s, bool is_positive) {

17
src/test/polysat.cpp
View file

@ -869,17 +869,13 @@ namespace polysat {
void tst_polysat() {
// not working
// polysat::test_fixed_point_arith_div_mul_inverse();
// polysat::test_cjust();
polysat::test_ineq_basic5();
// polysat::test_ineq_basic6();
// polysat::test_monot_bounds_full();
// polysat::test_monot_bounds_simple(8);
// working
polysat::test_cjust();
//polysat::test_monot_bounds_simple(8);
return;
// working
polysat::test_fixed_point_arith_mul_div_inverse();
polysat::test_subst();
polysat::test_monot_bounds(8);
@ -898,8 +894,13 @@ void tst_polysat() {
polysat::test_ineq_basic2();
polysat::test_ineq_basic3();
polysat::test_ineq_basic4();
polysat::test_ineq_basic5();
polysat::test_ineq_basic6();
polysat::test_monot_bounds(2);
// inefficient conflicts:
// Takes time: polysat::test_monot_bounds_full();
#if 0
// worry about this later
polysat::test_ineq1();