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

No more boolean decisions

Browse source
This commit is contained in:
Jakob Rath 2022-08-04 14:12:12 +02:00
parent c67024d88b
commit d5f20dcf0e
2 changed files with 20 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/math/polysat/boolean.cpp
View file

@ -25,19 +25,22 @@ namespace polysat {
m_level.push_back(UINT_MAX);
m_deps.push_back(null_dependency);
m_kind.push_back(kind_t::unassigned);
m_clause.push_back(nullptr);
m_reason.push_back(nullptr);
m_watch.push_back({});
m_watch.push_back({});
}
else {
var = m_unused.back();
m_unused.pop_back();
auto lit = sat::literal(var);
SASSERT_EQ(m_value[lit.index()], l_undef);
SASSERT_EQ(m_value[(~lit).index()], l_undef);
SASSERT_EQ(m_level[var], UINT_MAX);
SASSERT_EQ(m_value[2*var], l_undef);
SASSERT_EQ(m_value[2*var+1], l_undef);
SASSERT_EQ(m_kind[var], kind_t::unassigned);
SASSERT_EQ(m_clause[var], nullptr);
SASSERT_EQ(m_deps[var], null_dependency);
SASSERT_EQ(m_kind[var], kind_t::unassigned);
SASSERT_EQ(m_reason[var], nullptr);
SASSERT(m_watch[lit.index()].empty());
SASSERT(m_watch[(~lit).index()].empty());
}
return var;
}
@ -49,7 +52,7 @@ namespace polysat {
m_value[(~lit).index()] = l_undef;
m_level[var] = UINT_MAX;
m_kind[var] = kind_t::unassigned;
m_clause[var] = nullptr;
m_reason[var] = nullptr;
m_deps[var] = null_dependency;
m_watch[lit.index()].reset();
m_watch[(~lit).index()].reset();
@ -63,12 +66,6 @@ namespace polysat {
SASSERT(is_bool_propagation(lit));
}
void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause& lemma) {
LOG("Decide literal " << lit << " @ " << lvl);
assign(kind_t::decision, lit, lvl, &lemma);
SASSERT(is_decision(lit));
}
void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
LOG("Eval literal " << lit << " @ " << lvl);
assign(kind_t::value_propagation, lit, lvl, nullptr);
@ -78,7 +75,7 @@ namespace polysat {
void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) {
LOG("Asserted " << lit << " @ " << lvl);
assign(kind_t::assumption, lit, lvl, nullptr, dep);
SASSERT(is_decision(lit) || is_assumption(lit));
SASSERT(is_assumption(lit));
}
void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) {
@ -88,7 +85,7 @@ namespace polysat {
m_value[(~lit).index()] = l_false;
m_level[lit.var()] = lvl;
m_kind[lit.var()] = k;
m_clause[lit.var()] = reason;
m_reason[lit.var()] = reason;
m_deps[lit.var()] = dep;
}
@ -98,7 +95,7 @@ namespace polysat {
m_value[(~lit).index()] = l_undef;
m_level[lit.var()] = UINT_MAX;
m_kind[lit.var()] = kind_t::unassigned;
m_clause[lit.var()] = nullptr;
m_reason[lit.var()] = nullptr;
m_deps[lit.var()] = null_dependency;
}

28
src/math/polysat/boolean.h
View file

@ -25,25 +25,19 @@ namespace polysat {
bool_propagation,
value_propagation,
assumption,
decision,
};
svector<sat::bool_var> m_unused; // previously deleted variables that can be reused by new_var();
svector<lbool> m_value; // current value (indexed by literal)
unsigned_vector m_level; // level of assignment (indexed by variable)
dependency_vector m_deps; // dependencies of external asserts
svector<kind_t> m_kind; // decision or propagation?
// Clause associated with the assignment (indexed by variable):
// - for propagations: the reason (or NULL for eval'd literals)
// - for decisions: the lemma (or NULL for externally asserted literals)
ptr_vector<clause> m_clause;
vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses
svector<sat::bool_var> m_unused; // previously deleted variables that can be reused by new_var();
svector<lbool> m_value; // current value (indexed by literal)
unsigned_vector m_level; // level of assignment (indexed by variable)
dependency_vector m_deps; // dependencies of external asserts
svector<kind_t> m_kind; // decision or propagation?
ptr_vector<clause> m_reason; // reasons for bool-propagated literals
vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses
void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep = null_dependency);
public:
bool_var_manager() {}
// allocated size (not the number of active variables)
@ -54,8 +48,6 @@ namespace polysat {
bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; }
bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; }
bool is_decision(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::decision; }
bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
bool is_assumption(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::assumption; }
bool is_assumption(sat::literal lit) const { return is_assumption(lit.var()); }
bool is_bool_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::bool_propagation; }
@ -68,17 +60,14 @@ namespace polysat {
bool is_false(sat::literal lit) const { return value(lit) == l_false; }
unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; }
unsigned level(sat::literal lit) const { return level(lit.var()); }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_bool_propagation(var) ? m_clause[var] : nullptr; }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); SASSERT(is_bool_propagation(var) == !!m_reason[var]); return m_reason[var]; }
clause* reason(sat::literal lit) const { return reason(lit.var()); }
dependency dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; }
ptr_vector<clause>& watch(sat::literal lit) { return m_watch[lit.index()]; }
/// Set the given literal to true
void propagate(sat::literal lit, unsigned lvl, clause& reason);
void decide(sat::literal lit, unsigned lvl, clause& lemma);
void eval(sat::literal lit, unsigned lvl);
void assumption(sat::literal lit, unsigned lvl, dependency dep);
void unassign(sat::literal lit);
@ -91,7 +80,6 @@ namespace polysat {
case kind_t::unassigned: return out << "unassigned";
case kind_t::bool_propagation: return out << "bool propagation";
case kind_t::value_propagation: return out << "value propagation";
case kind_t::decision: return out << "decision";
case kind_t::assumption: return out << "assumption";
default: UNREACHABLE(); return out;
}