mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Fix name: value propagation -> evaluation (for boolean literals)

Browse source
This commit is contained in:
Jakob Rath 2022-11-14 14:58:20 +01:00
parent 436881c18c
commit eec8e8ebe4
5 changed files with 15 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -73,8 +73,8 @@ namespace polysat {
void bool_var_manager::eval(sat::literal lit, unsigned lvl) {
LOG_V("Eval literal " << lit << " @ " << lvl);
assign(kind_t::value_propagation, lit, lvl, nullptr);
SASSERT(is_value_propagation(lit));
assign(kind_t::evaluation, lit, lvl, nullptr);
SASSERT(is_evaluation(lit));
}
void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) {

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

@ -22,10 +22,13 @@ namespace polysat {
enum class kind_t {
unassigned,
bool_propagation,
value_propagation,
assumption,
decision,
/// input constraint
assumption,
/// propagated due to boolean clause
bool_propagation,
/// evaluated under pvar assignment
evaluation,
};
svector<sat::bool_var> m_unused; // previously deleted variables that can be reused by new_var();
@ -57,8 +60,8 @@ namespace polysat {
bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
bool is_bool_propagation(sat::bool_var var) const { SASSERT(invariant(var)); return m_kind[var] == kind_t::bool_propagation; }
bool is_bool_propagation(sat::literal lit) const { return is_bool_propagation(lit.var()); }
bool is_value_propagation(sat::bool_var var) const { SASSERT(invariant(var)); return m_kind[var] == kind_t::value_propagation; }
bool is_value_propagation(sat::literal lit) const { return is_value_propagation(lit.var()); }
bool is_evaluation(sat::bool_var var) const { SASSERT(invariant(var)); return m_kind[var] == kind_t::evaluation; }
bool is_evaluation(sat::literal lit) const { return is_evaluation(lit.var()); }
lbool value(sat::bool_var var) const { return value(sat::literal(var)); }
lbool value(sat::literal lit) const { return m_value[lit.index()]; }
bool is_true(sat::literal lit) const { return value(lit) == l_true; }
@ -86,7 +89,7 @@ namespace polysat {
switch (k) {
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::evaluation: return out << "evaluation";
case kind_t::assumption: return out << "assumption";
case kind_t::decision: return out << "decision";
}

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

@ -401,7 +401,7 @@ namespace polysat {
// The reason for lit is conceptually:
// x1 = v1 /\ ... /\ xn = vn ==> lit
SASSERT(s.m_bvars.is_value_propagation(lit));
SASSERT(s.m_bvars.is_evaluation(lit));
SASSERT(contains(lit));
SASSERT(!contains(~lit));

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

@ -50,7 +50,7 @@ namespace polysat {
out << "\n\t" << rpad(4, l2) << ": " << rpad(16, s.lit2cnstr(l2)) << " " << bool_justification_pp(s.m_bvars, l2);
}
}
else if (s.m_bvars.is_value_propagation(lit)) {
else if (s.m_bvars.is_evaluation(lit)) {
out << " evaluated";
}
else {

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

@ -733,7 +733,7 @@ namespace polysat {
if (m_bvars.is_bool_propagation(var))
m_conflict.resolve_bool(lit, *m_bvars.reason(lit));
else {
SASSERT(m_bvars.is_value_propagation(var));
SASSERT(m_bvars.is_evaluation(var));
m_conflict.resolve_with_assignment(lit);
}
}
@ -1188,7 +1188,7 @@ namespace polysat {
out << "assert";
else if (s.m_bvars.is_bool_propagation(lit))
out << "bprop";
else if (s.m_bvars.is_value_propagation(lit))
else if (s.m_bvars.is_evaluation(lit))
out << "eval";
else if (s.m_bvars.is_decision(lit))
out << "decide";