mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #4541

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-24 20:26:42 -07:00
parent 8d16a9a034
commit 85cb0293f5
3 changed files with 7 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/sat/ba_solver.cpp
View file

@ -1177,6 +1177,7 @@ namespace sat {
do { do {
if (m_overflow || offset > (1 << 12)) { if (m_overflow || offset > (1 << 12)) {
IF_VERBOSE(20, verbose_stream() << "offset: " << offset << "\n"; IF_VERBOSE(20, verbose_stream() << "offset: " << offset << "\n";
DEBUG_CODE(active2pb(m_A); display(verbose_stream(), m_A););); DEBUG_CODE(active2pb(m_A); display(verbose_stream(), m_A);););
@ -1214,7 +1215,7 @@ namespace sat {
case justification::TERNARY: case justification::TERNARY:
inc_bound(offset); inc_bound(offset);
SASSERT (consequent != null_literal); SASSERT (consequent != null_literal);
inc_coeff(consequent, offset); inc_coeff(consequent, offset);
process_antecedent(js.get_literal1(), offset); process_antecedent(js.get_literal1(), offset);
process_antecedent(js.get_literal2(), offset); process_antecedent(js.get_literal2(), offset);
break; break;

2
src/sat/sat_justification.h
View file

@ -23,7 +23,7 @@ namespace sat {
class justification { class justification {
public: public:
enum kind { NONE, BINARY, TERNARY, CLAUSE, EXT_JUSTIFICATION }; enum kind { NONE = 0, BINARY = 1, TERNARY = 2, CLAUSE = 3, EXT_JUSTIFICATION = 4};
private: private:
unsigned m_level; unsigned m_level;
size_t m_val1; size_t m_val1;

16
src/sat/sat_solver.cpp
View file

@ -429,21 +429,13 @@ namespace sat {
bool solver::propagate_bin_clause(literal l1, literal l2) { bool solver::propagate_bin_clause(literal l1, literal l2) {
if (value(l2) == l_false) { if (value(l2) == l_false) {
if (value(l1) == l_false) { m_stats.m_bin_propagate++;
TRACE("sat", tout << "conflict " << l1 << " " << l2 << "\n";); assign(l1, justification(lvl(l2), l2));
set_conflict(justification(std::max(lvl(l1), lvl(l2)), l1, l2));
}
else {
m_stats.m_bin_propagate++;
//TRACE("sat", tout << "propagate " << l1 << " <- " << ~l2 << "\n";);
assign(l1, justification(lvl(l2), l2));
}
return true; return true;
} }
else if (value(l1) == l_false) { if (value(l1) == l_false) {
m_stats.m_bin_propagate++; m_stats.m_bin_propagate++;
//TRACE("sat", tout << "propagate " << l2 << " <- " << ~l1 << "\n";); assign(l2, justification(lvl(l1), l1));
assign(l2, justification(lvl(l1), l1) );
return true; return true;
} }
return false; return false;