mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 17:30:23 +00:00
Code Activity

fixes to bdd

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-14 16:49:04 -07:00 • committed by Arie Gurfinkel
parent 05abf19009
commit a0af3383db
4 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/qe/qe_mbi.cpp
View file

@ -259,7 +259,7 @@ namespace qe {
app_ref_vector& m_vars; app_ref_vector& m_vars;
arith_util arith; arith_util arith;
obj_hashtable<func_decl> m_exclude; obj_hashtable<func_decl> m_exclude;
is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared):
m(vars.m()), m_vars(vars), arith(m) { m(vars.m()), m_vars(vars), arith(m) {
for (func_decl* f : shared) m_exclude.insert(f); for (func_decl* f : shared) m_exclude.insert(f);
} }
@ -317,8 +317,8 @@ namespace qe {
app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) { app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) {
arith_util a(m); arith_util a(m);
app_ref_vector avars(m); app_ref_vector avars(m);
is_arith_var_proc _proc(avars, m_shared); is_arith_var_proc _proc(avars, m_shared);
for_each_expr(_proc, lits); for_each_expr(_proc, lits);
return avars; return avars;
} }
@ -484,7 +484,7 @@ namespace qe {
return l_true, mbp of local, mdl of local & blocked return l_true, mbp of local, mdl of local & blocked
else if !is_sat(local & lits) then else if !is_sat(local & lits) then
return l_false, mbp of local, nullptr return l_false, mbp of local, nullptr
else if is_sat(local & lits) && !is_sat(local & lits & blocked) else // is_sat(local & lits) && !is_sat(local & lits & blocked)
MISSING CASE MISSING CASE
MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked MUST PRODUCE AN IMPLICANT OF LOCAL that is inconsistent with lits & blocked
in this case !is_sat(local & lits & mdl) and is_sat(mdl, blocked) in this case !is_sat(local & lits & mdl) and is_sat(mdl, blocked)

2
src/sat/ba_solver.cpp
View file

@ -556,7 +556,7 @@ namespace sat {
bool is_false = false; bool is_false = false;
for (unsigned k = 0; k < sz; ++k) { for (unsigned k = 0; k < sz; ++k) {
SASSERT(!is_false || value(p[k].second) == l_false); SASSERT(!is_false || value(p[k].second) == l_false);
SASSERT(k < j == (value(p[k].second) != l_false)); SASSERT((k < j) == (value(p[k].second) != l_false));
is_false = value(p[k].second) == l_false; is_false = value(p[k].second) == l_false;
}); });

10
src/sat/sat_bdd.cpp
View file

@ -108,7 +108,7 @@ namespace sat {
bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) { bool bdd_manager::check_result(op_entry*& e1, op_entry const* e2, BDD a, BDD b, BDD c) {
if (e1 != e2) { if (e1 != e2) {
SASSERT(e2->m_result != -1); SASSERT(e2->m_result != null_bdd);
push_entry(e1); push_entry(e1);
e1 = nullptr; e1 = nullptr;
return true; return true;
@ -117,7 +117,7 @@ namespace sat {
e1->m_bdd1 = a; e1->m_bdd1 = a;
e1->m_bdd2 = b; e1->m_bdd2 = b;
e1->m_op = c; e1->m_op = c;
SASSERT(e1->m_result == -1); SASSERT(e1->m_result == null_bdd);
return false; return false;
} }
} }
@ -203,7 +203,7 @@ namespace sat {
void * mem = m_alloc.allocate(sizeof(op_entry)); void * mem = m_alloc.allocate(sizeof(op_entry));
result = new (mem) op_entry(l, r, op); result = new (mem) op_entry(l, r, op);
} }
result->m_result = -1; result->m_result = null_bdd;
return result; return result;
} }
@ -667,7 +667,7 @@ namespace sat {
r = e2->m_result; r = e2->m_result;
} }
else { else {
SASSERT(e1->m_result == -1); SASSERT(e1->m_result == null_bdd);
push(mk_quant_rec(l, lo(b), op)); push(mk_quant_rec(l, lo(b), op));
push(mk_quant_rec(l, hi(b), op)); push(mk_quant_rec(l, hi(b), op));
r = make_node(lvl, read(2), read(1)); r = make_node(lvl, read(2), read(1));
@ -782,7 +782,7 @@ namespace sat {
ptr_vector<op_entry> to_delete, to_keep; ptr_vector<op_entry> to_delete, to_keep;
for (auto* e : m_op_cache) { for (auto* e : m_op_cache) {
if (e->m_result != -1) { if (e->m_result != null_bdd) {
to_delete.push_back(e); to_delete.push_back(e);
} }
else { else {

2
src/sat/sat_bdd.h
View file

@ -32,6 +32,8 @@ namespace sat {
typedef unsigned BDD; typedef unsigned BDD;
const BDD null_bdd = UINT_MAX;
enum bdd_op { enum bdd_op {
bdd_and_op = 2, bdd_and_op = 2,
bdd_or_op = 3, bdd_or_op = 3,