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

fix bug in Shannon decomposition for translating PB constraints into formulas

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-01 12:51:40 -07:00
parent 5dc2afa33f
commit cce287eed1
4 changed files with 20 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -335,6 +335,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
SASSERT(num == 2);
if (butil().is_bv(args[0])) {
reduce_eq(args[0], args[1], result);
std::cout << "reduce eq: " << mk_pp(args[0], m()) << "\n" << mk_pp(args[1], m()) << "\n";
std::cout << mk_pp(result, m()) << "\n";
return BR_DONE;
}
return BR_FAILED;

3
src/smt/smt_context.cpp
View file

@ -2872,7 +2872,7 @@ namespace smt {
// mark_as_relevant(l); <<< not needed
// internalize_assertion marked l as relevant.
SASSERT(is_relevant(l));
TRACE("assumptions", tout << mk_pp(curr_assumption, m_manager) << "\n";);
TRACE("assumptions", tout << l << ":" << mk_pp(curr_assumption, m_manager) << "\n";);
if (m_manager.proofs_enabled())
assign(l, mk_justification(justification_proof_wrapper(*this, pr)));
else
@ -2907,6 +2907,7 @@ namespace smt {
literal l = *it;
TRACE("unsat_core_bug", tout << "answer literal: " << l << "\n";);
SASSERT(get_bdata(l.var()).m_assumption);
if (!m_literal2assumption.contains(l.index())) l.neg();
SASSERT(m_literal2assumption.contains(l.index()));
expr * a = m_literal2assumption[l.index()];
if (!already_found_assumptions.contains(a)) {

14
src/tactic/arith/card2bv_tactic.cpp
View file

@ -221,6 +221,7 @@ namespace pb {
default:
UNREACHABLE();
}
TRACE("card2bv", tout << result << "\n";);
}
struct argc_t {
@ -268,6 +269,8 @@ namespace pb {
SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff);
}
);
result = m.mk_app(f, sz, args);
TRACE("card2bv", tout << result << "\n";);
argc_cache cache;
expr_ref_vector trail(m);
vector<rational> todo_k;
@ -277,7 +280,7 @@ namespace pb {
decl_kind kind = f->get_decl_kind();
argc_entry entry1;
while (!todo_i.empty()) {
SASSERT(todo_i.size() == todo_k.size());
if (cache.size() > max_clauses) {
return BR_FAILED;
}
@ -307,13 +310,17 @@ namespace pb {
break;
case OP_AT_LEAST_K:
case OP_PB_GE:
if (coeff < k) {
if (k.is_zero()) {
entry.m_value = m.mk_true();
}
else if (coeff < k) {
entry.m_value = m.mk_false();
}
else if (coeff.is_zero()) {
entry.m_value = m.mk_true();
}
else {
SASSERT(coeff >= k && k.is_pos());
entry.m_value = arg;
}
break;
@ -345,7 +352,7 @@ namespace pb {
todo_k.push_back(k);
}
entry.m_k -= coeff;
if (kind != OP_PB_EQ && entry.m_k.is_neg()) {
if (kind != OP_PB_EQ && !entry.m_k.is_pos()) {
switch (kind) {
case OP_AT_MOST_K:
case OP_PB_LE:
@ -379,6 +386,7 @@ namespace pb {
argc_entry entry(0, pb.get_k(f));
VERIFY(cache.find(entry, entry));
result = entry.m_value;
TRACE("card2bv", tout << result << "\n";);
return BR_DONE;
}

6
src/tactic/tactic.cpp
View file

@ -41,11 +41,13 @@ struct tactic_report::imp {
goal const & m_goal;
stopwatch m_watch;
double m_start_memory;
unsigned m_start_exprs;
imp(char const * id, goal const & g):
m_id(id),
m_goal(g),
m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)) {
m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)),
m_start_exprs(g.num_exprs()){
m_watch.start();
}
@ -53,7 +55,7 @@ struct tactic_report::imp {
m_watch.stop();
double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
verbose_stream() << "(" << m_id
<< " :num-exprs " << m_goal.num_exprs()
<< " :num-exprs " << m_start_exprs << " -> " << m_goal.num_exprs()
<< " :num-asts " << m_goal.m().get_num_asts()
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
<< " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory