mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

bugbash

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-09 15:30:33 -08:00
parent 3e23ff9bad
commit e2c5d7d358
3 changed files with 15 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/ast/euf/euf_bv_plugin.cpp
View file

@ -259,17 +259,24 @@ namespace euf {
void bv_plugin::propagate_register_node(enode* n) {
TRACE("bv", tout << "register " << g.bpp(n) << "\n");
auto& i = info(n);
i.value = n;
enode* a, * b;
unsigned lo, hi;
if (is_concat(n, a, b)) {
auto& i = info(n);
i.value = n;
i.hi = a;
i.lo = b;
i.cut = width(b);
push_undo_split(n);
}
unsigned lo, hi;
if (is_extract(n, lo, hi) && (lo != 0 || hi + 1 != width(n->get_arg(0)))) {
else if (is_concat(n) && n->num_args() != 2) {
SASSERT(n->num_args() != 0);
auto last = n->get_arg(n->num_args() - 1);
for (unsigned i = n->num_args() - 1; i-- > 0;)
last = mk_concat(n->get_arg(i), last);
push_merge(last, n);
}
else if (is_extract(n, lo, hi) && (lo != 0 || hi + 1 != width(n->get_arg(0)))) {
enode* arg = n->get_arg(0);
unsigned w = width(arg);
if (all_of(enode_parents(arg), [&](enode* p) { unsigned _lo, _hi; return !is_extract(p, _lo, _hi) || _lo != 0 || _hi + 1 != w; }))

1
src/sat/smt/polysat_internalize.cpp
View file

@ -669,7 +669,6 @@ namespace polysat {
SASSERT(bv.is_concat(e));
SASSERT(e->get_num_args() > 0);
sat::literal_vector neqs;
verbose_stream() << mk_pp(e, m) << "\n";
expr* hi = e->get_arg(e->get_num_args() - 1);
auto sz_e = bv.get_bv_size(e);
auto sz_h = bv.get_bv_size(hi);

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

@ -135,7 +135,9 @@ namespace polysat {
}
void solver::explain_dep(dependency const& d, euf::enode_pair_vector& eqs, sat::literal_vector& core) {
if (d.is_bool_var()) {
if (d.is_axiom())
;
else if (d.is_bool_var()) {
auto bv = d.bool_var();
auto lit = sat::literal(bv, s().value(bv) == l_false);
core.push_back(lit);
@ -379,7 +381,7 @@ namespace polysat {
core.push_back(~lit);
hint = mk_proof_hint(name, core, {});
}
IF_VERBOSE(1, display_clause(name, verbose_stream(), lits));
IF_VERBOSE(3, display_clause(name, verbose_stream(), lits));
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
}