mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

fix build

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 13:37:17 +02:00
parent 6ffcea0bde
commit 412b6ffd4a
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -146,6 +146,12 @@ namespace polysat {
m_constraints.shrink(j); m_constraints.shrink(j);
} }
void conflict_core::set_bailout() {
SASSERT(!is_bailout());
m_bailout = true;
s().m_stats.m_num_bailouts++;
}
void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) { void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z // Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
// clause: x \/ u \/ v // clause: x \/ u \/ v

2
src/math/polysat/conflict_core.h
View file

@ -68,7 +68,7 @@ namespace polysat {
pvar conflict_var() const { return m_conflict_var; } pvar conflict_var() const { return m_conflict_var; }
bool is_bailout() const { return m_bailout; } bool is_bailout() const { return m_bailout; }
void set_bailout() { SASSERT(!is_bailout()); m_bailout = true; s().m_stats.m_num_bailouts++; } void set_bailout();
bool empty() const { bool empty() const {
return m_constraints.empty() && m_vars.empty() && m_literals.empty() && m_conflict_var == null_var; return m_constraints.empty() && m_vars.empty() && m_literals.empty() && m_conflict_var == null_var;