mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

improve diagnostics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-04 11:07:09 -08:00
parent 7b0c04a3e8
commit 5fc208cefc
4 changed files with 22 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/sat/smt/polysat_solver.cpp
View file

@ -345,8 +345,8 @@ namespace polysat {
TRACE("bv", tout << "literal is true " << ctx.literal2expr(lit) << "\n");
return false;
}
TRACE("bv", tout << name << ": "; for (auto lit : lits) tout << ctx.literal2expr(lit) << " "; tout << "\n");
IF_VERBOSE(1, verbose_stream() << name << ": "; for (auto lit : lits) verbose_stream() << ctx.literal2expr(lit) << " "; verbose_stream() << "\n");
TRACE("bv", display_clause(name, tout, lits));
IF_VERBOSE(1, display_clause(name, verbose_stream(), lits));
validate_axiom(lits);
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
return true;
@ -368,7 +368,17 @@ namespace polysat {
lits.push_back(lit);
}
validate_axiom(lits);
IF_VERBOSE(1, verbose_stream() << name << ": "; for (auto lit : lits) verbose_stream() << ctx.literal2expr(lit) << " "; verbose_stream() << "\n");
unsigned j = 0;
for (auto lit : lits) {
if (s().value(lit) == l_true && s().lvl(lit) == 0)
return;
if (s().value(lit) == l_false && s().lvl(lit) == 0)
continue;
lits[j++] = lit;
}
lits.shrink(j);
IF_VERBOSE(1, display_clause(name, verbose_stream(), lits));
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
}