mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

debugging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-27 13:18:20 -07:00
parent 94416bea52
commit 6f4c873b29
9 changed files with 139 additions and 102 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

186
src/sat/card_extension.cpp
View file

@ -281,106 +281,109 @@ namespace sat {
for (unsigned i = 0; i < num_watch; ++i) {
watch_literal(p, p[i]);
}
p.set_slack(slack);
p.set_num_watch(num_watch);
}
TRACE("sat", display(tout << "init watch: ", p, true););
}
p.set_slack(slack);
p.set_num_watch(num_watch);
}
TRACE("sat", display(tout << "init watch: ", p, true););
}
/*
Chai Kuhlmann:
Lw - set of watched literals
Lu - set of unwatched literals that are not false
Lw = Lw \ { alit }
Sw -= value
a_max = max { a | l in Lw u Lu, l = undef }
while (Sw < k + a_max & Lu != 0) {
a_s = max { a | l in Lu }
Sw += a_s
Lw = Lw u {l_s}
Lu = Lu \ {l_s}
}
if (Sw < k) conflict
while (Sw < k + a_max) {
assign (l_max)
a_max = max { ai | li in Lw, li = undef }
}
ASSERT(Sw >= bound)
return no-conflict
/*
Chai Kuhlmann:
Lw - set of watched literals
Lu - set of unwatched literals that are not false
a_max index: index of non-false literal with maximal weight.
*/
void card_extension::add_index(pb& p, unsigned index, literal lit) {
if (value(lit) == l_undef) {
m_pb_undef.push_back(index);
if (p[index].first > m_a_max) {
m_a_max = p[index].first;
}
}
}
Lw = Lw \ { alit }
Sw -= value
a_max = max { a | l in Lw u Lu, l = undef }
while (Sw < k + a_max & Lu != 0) {
a_s = max { a | l in Lu }
Sw += a_s
Lw = Lw u {l_s}
Lu = Lu \ {l_s}
}
if (Sw < k) conflict
while (Sw < k + a_max) {
assign (l_max)
a_max = max { ai | li in Lw, li = undef }
}
ASSERT(Sw >= bound)
return no-conflict
lbool card_extension::add_assign(pb& p, literal alit) {
a_max index: index of non-false literal with maximal weight.
TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
SASSERT(!inconsistent());
unsigned sz = p.size();
unsigned bound = p.k();
unsigned num_watch = p.num_watch();
unsigned slack = p.slack();
SASSERT(value(alit) == l_false);
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
SASSERT(num_watch <= sz);
SASSERT(num_watch > 0);
unsigned index = 0;
m_a_max = 0;
m_pb_undef.reset();
for (; index < num_watch; ++index) {
literal lit = p[index].second;
if (lit == alit) {
break;
}
add_index(p, index, lit);
}
SASSERT(index < num_watch);
unsigned index1 = index + 1;
for (; m_a_max == 0 && index1 < num_watch; ++index1) {
add_index(p, index1, p[index1].second);
}
*/
void card_extension::add_index(pb& p, unsigned index, literal lit) {
if (value(lit) == l_undef) {
m_pb_undef.push_back(index);
if (p[index].first > m_a_max) {
m_a_max = p[index].first;
}
}
}
unsigned val = p[index].first;
SASSERT(value(p[index].second) == l_false);
SASSERT(val <= slack);
slack -= val;
// find literals to swap with:
for (unsigned j = num_watch; j < sz && slack < bound + m_a_max; ++j) {
literal lit = p[j].second;
if (value(lit) != l_false) {
slack += p[j].first;
watch_literal(p, p[j]);
p.swap(num_watch, j);
add_index(p, num_watch, lit);
++num_watch;
}
}
lbool card_extension::add_assign(pb& p, literal alit) {
SASSERT(!inconsistent());
DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); });
TRACE("sat", display(tout << "assign: " << alit << "\n", p, true););
SASSERT(!inconsistent());
unsigned sz = p.size();
unsigned bound = p.k();
unsigned num_watch = p.num_watch();
unsigned slack = p.slack();
SASSERT(value(alit) == l_false);
SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
SASSERT(num_watch <= sz);
SASSERT(num_watch > 0);
unsigned index = 0;
m_a_max = 0;
m_pb_undef.reset();
for (; index < num_watch; ++index) {
literal lit = p[index].second;
if (lit == alit) {
break;
}
add_index(p, index, lit);
}
SASSERT(index < num_watch);
if (slack < bound) {
// maintain watching the literal
slack += val;
p.set_slack(slack);
p.set_num_watch(num_watch);
SASSERT(bound <= slack);
TRACE("sat", tout << "conflict " << alit << "\n";);
set_conflict(p, alit);
return l_false;
}
unsigned index1 = index + 1;
for (; m_a_max == 0 && index1 < num_watch; ++index1) {
add_index(p, index1, p[index1].second);
}
unsigned val = p[index].first;
SASSERT(value(p[index].second) == l_false);
SASSERT(val <= slack);
slack -= val;
// find literals to swap with:
for (unsigned j = num_watch; j < sz && slack < bound + m_a_max; ++j) {
literal lit = p[j].second;
if (value(lit) != l_false) {
slack += p[j].first;
watch_literal(p, p[j]);
p.swap(num_watch, j);
add_index(p, num_watch, lit);
++num_watch;
}
}
SASSERT(!inconsistent());
DEBUG_CODE(for (auto idx : m_pb_undef) { SASSERT(value(p[idx].second) == l_undef); });
if (slack < bound) {
// maintain watching the literal
slack += val;
p.set_slack(slack);
p.set_num_watch(num_watch);
SASSERT(bound <= slack);
TRACE("sat", tout << "conflict " << alit << "\n";);
set_conflict(p, alit);
return l_false;
}
if (index > p.size() || num_watch > p.size()) {
std::cout << "size: " << p.size() << "index: " << index << " num watch: " << num_watch << "\n";
}
// swap out the watched literal.
--num_watch;
SASSERT(num_watch > 0);
@ -1711,6 +1714,7 @@ namespace sat {
}
void card_extension::simplify() {
return;
s().pop_to_base_level();
unsigned trail_sz;
do {

5
src/sat/sat_lookahead.cpp
View file

@ -1734,11 +1734,14 @@ namespace sat {
}
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_units << ")\n";);
if (num_units > 0 && !m_s.inconsistent()) {
if (m_s.inconsistent()) return;
if (num_units > 0) {
m_s.propagate_core(false);
m_s.m_simplifier(false);
}
m_lookahead.reset();
}
//

2
src/sat/sat_model_converter.cpp
View file

@ -162,7 +162,7 @@ namespace sat {
for (unsigned i = 0; i < sz; ++i)
e.m_clauses.push_back(c[i]);
e.m_clauses.push_back(null_literal);
TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
// TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
}
bool model_converter::check_invariant(unsigned num_vars) const {

16
src/sat/sat_solver.cpp
View file

@ -1415,10 +1415,16 @@ namespace sat {
}
if (m_config.m_lookahead_simplify) {
lookahead lh(*this);
lh.simplify();
lh.scc();
lh.collect_statistics(m_aux_stats);
{
lookahead lh(*this);
lh.simplify();
lh.collect_statistics(m_aux_stats);
}
{
lookahead lh(*this);
lh.scc();
lh.collect_statistics(m_aux_stats);
}
}
sort_watch_lits();
@ -1450,7 +1456,7 @@ namespace sat {
m_next_simplify = m_conflicts_since_init + m_config.m_simplify_max;
}
#if 1
#if 0
static unsigned file_no = 0;
#pragma omp critical (print_sat)
{

13
src/tactic/arith/bound_manager.cpp
View file

@ -28,6 +28,19 @@ bound_manager::~bound_manager() {
reset();
}
bound_manager* bound_manager::translate(ast_manager& dst_m) {
bound_manager* result = alloc(bound_manager, dst_m);
ast_translation tr(m(), dst_m);
expr_dependency_translation edtr(tr);
for (auto& kv : m_lowers) result->m_lowers.insert(tr(kv.m_key), kv.m_value);
for (auto& kv : m_uppers) result->m_uppers.insert(tr(kv.m_key), kv.m_value);
for (auto& kv : m_lower_deps) result->m_lower_deps.insert(tr(kv.m_key), edtr(kv.m_value));
for (auto& kv : m_upper_deps) result->m_upper_deps.insert(tr(kv.m_key), edtr(kv.m_value));
for (expr* e : m_bounded_vars) result->m_bounded_vars.push_back(tr(e));
return result;
}
static decl_kind swap_decl(decl_kind k) {
switch (k) {
case OP_LE: return OP_GE;

2
src/tactic/arith/bound_manager.h
View file

@ -47,6 +47,8 @@ public:
bound_manager(ast_manager & m);
~bound_manager();
bound_manager* translate(ast_manager& dst_m);
ast_manager & m() const { return m_util.get_manager(); }
void operator()(goal const & g);

13
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -73,8 +73,17 @@ public:
}
}
virtual solver* translate(ast_manager& m, params_ref const& p) {
return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p));
virtual solver* translate(ast_manager& dst_m, params_ref const& p) {
flush_assertions();
bounded_int2bv_solver* result = alloc(bounded_int2bv_solver, dst_m, p, m_solver->translate(dst_m, p));
ast_translation tr(m, dst_m);
for (auto& kv : m_int2bv) result->m_int2bv.insert(tr(kv.m_key), tr(kv.m_value));
for (auto& kv : m_bv2int) result->m_bv2int.insert(tr(kv.m_key), tr(kv.m_value));
for (auto& kv : m_bv2offset) result->m_bv2offset.insert(tr(kv.m_key), kv.m_value);
for (func_decl* f : m_bv_fns) result->m_bv_fns.push_back(tr(f));
for (func_decl* f : m_int_fns) result->m_int_fns.push_back(tr(f));
for (bound_manager* b : m_bounds) result->m_bounds.push_back(b->translate(dst_m));
return result;
}
virtual void assert_expr(expr * t) {

2
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -50,7 +50,7 @@ public:
virtual ~enum2bv_solver() {}
virtual solver* translate(ast_manager& m, params_ref const& p) {
virtual solver* translate(ast_manager& m, params_ref const& p) {
return alloc(enum2bv_solver, m, p, m_solver->translate(m, p));
}

2
src/tactic/portfolio/pb2bv_solver.cpp
View file

@ -49,7 +49,7 @@ public:
virtual ~pb2bv_solver() {}
virtual solver* translate(ast_manager& m, params_ref const& p) {
flush_assertions();
return alloc(pb2bv_solver, m, p, m_solver->translate(m, p));
}