mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

remove last references to unit clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-20 17:36:07 -07:00
parent cd76fd9edd
commit ce12c51083
5 changed files with 2 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/clause_builder.cpp
View file

@ -57,9 +57,11 @@ namespace polysat {
SASSERT(c);
SASSERT(c->has_bvar());
SASSERT(!c.is_always_true()); // clause would be a tautology
#if 0
if (c->unit_clause()) {
return;
}
#endif
m_literals.push_back(c.blit());
}

2
src/math/polysat/conflict.cpp
View file

@ -209,8 +209,6 @@ namespace polysat {
c_lemma.push(c.blit());
clause_ref lemma = c_lemma.build();
cm().store(lemma.get(), s());
if (lemma->size() == 1)
c->set_unit_clause(lemma.get());
if (s().m_bvars.value(c.blit()) == l_undef)
s().assign_bool(s().level(*lemma), c.blit(), lemma.get(), nullptr);
}

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

@ -263,11 +263,6 @@ namespace polysat {
narrow(s, is_positive);
}
void constraint::set_unit_clause(clause *cl) {
// can be seen as a cache... store the lowest-level unit clause for this constraint.
if (!cl || !m_unit_clause)
m_unit_clause = cl;
}
unsigned constraint::level(solver& s) const {
if (s.m_bvars.value(sat::literal(bvar())) != l_undef)

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

@ -131,7 +131,6 @@ namespace polysat {
friend class ule_constraint;
// constraint_manager* m_manager;
clause* m_unit_clause = nullptr; ///< If this constraint was asserted by a unit clause, we store that clause here.
ckind_t m_kind;
unsigned_vector m_vars;
lbool m_external_sign = l_undef;
@ -178,9 +177,6 @@ namespace polysat {
std::string bvar2string() const;
unsigned level(solver& s) const;
clause* unit_clause() const { return m_unit_clause; }
void set_unit_clause(clause* cl);
void set_external(bool sign) { m_external_sign = to_lbool(sign); }
void unset_external() { m_external_sign = l_undef; }
bool is_external() const { return m_external_sign != l_undef; }

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

@ -121,18 +121,9 @@ namespace polysat {
set_conflict(c /*, dep */);
return;
}
#if 0
clause_ref unit = clause::from_unit(c);
m_constraints.store(unit.get(), *this);
c->set_unit_clause(unit.get());
(void) dep; // dependencies go into justification
assign_bool(m_level, lit, c->unit_clause(), nullptr);
#else
// just add them as axioms, tracked by dependencies
m_bvars.assign(lit, m_level, nullptr, nullptr, dep);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);
#endif
#if ENABLE_LINEAR_SOLVER
m_linear_solver.new_constraint(*c.get());
@ -743,14 +734,8 @@ namespace polysat {
LOG(" Literal " << lit << " is: " << lit2cnstr(lit));
SASSERT(m_bvars.value(lit) != l_true);
}
if (lemma.empty())
std::cout << lemma << "\n";
SASSERT(!lemma.empty());
m_constraints.store(&lemma, *this);
if (lemma.size() == 1) {
signed_constraint c = lit2cnstr(lemma[0]);
c->set_unit_clause(&lemma);
}
propagate();
}