mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-14 22:41:56 -07:00
parent 9a2b7677bf
commit bb7754a767
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -209,11 +209,12 @@ namespace polysat {
} }
} }
auto p = c.p().subst_val(m_search); auto p = c.p().subst_val(m_search);
TRACE("polysat", tout << c.p() << " := " << p << "\n";);
if (p.is_zero()) if (p.is_zero())
return false; return false;
if (p.is_never_zero()) { if (p.is_never_zero()) {
TRACE("polysat", tout << c.p() << " := " << p << "\n";);
// we could tag constraint to allow early substitution before // we could tag constraint to allow early substitution before
// swapping watch variable in case we can detect conflict earlier. // swapping watch variable in case we can detect conflict earlier.
set_conflict(c); set_conflict(c);
@ -251,8 +252,10 @@ namespace polysat {
} }
void solver::propagate(pvar v, rational const& val, constraint& c) { void solver::propagate(pvar v, rational const& val, constraint& c) {
if (is_viable(v, val)) if (is_viable(v, val)) {
m_free_vars.del_var_eh(v);
assign_core(v, val, justification::propagation(m_level)); assign_core(v, val, justification::propagation(m_level));
}
else else
set_conflict(c); set_conflict(c);
} }
@ -356,6 +359,7 @@ namespace polysat {
++m_stats.m_num_decisions; ++m_stats.m_num_decisions;
else else
++m_stats.m_num_propagations; ++m_stats.m_num_propagations;
TRACE("polysat", tout << "v" << v << " := " << val << " " << j << "\n";);
SASSERT(is_viable(v, val)); SASSERT(is_viable(v, val));
m_value[v] = val; m_value[v] = val;
m_search.push_back(std::make_pair(v, val)); m_search.push_back(std::make_pair(v, val));