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

fix generation of wcnf

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-18 14:49:45 -08:00
parent 5083b1adee
commit 189d449cff
3 changed files with 60 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_solver.cpp
View file

@ -2917,6 +2917,7 @@ namespace sat {
++max_weight;
out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
out << "c soft " << sz << "\n";
for (unsigned i = 0; i < m_trail.size(); i++) {
out << max_weight << " " << dimacs_lit(m_trail[i]) << " 0\n";
@ -2940,9 +2941,9 @@ namespace sat {
clause_vector::const_iterator end = cs.end();
for (; it != end; ++it) {
clause const & c = *(*it);
unsigned sz = c.size();
unsigned clsz = c.size();
out << max_weight << " ";
for (unsigned j = 0; j < sz; j++)
for (unsigned j = 0; j < clsz; j++)
out << dimacs_lit(c[j]) << " ";
out << "0\n";
}
@ -2950,6 +2951,7 @@ namespace sat {
for (unsigned i = 0; i < sz; ++i) {
out << weights[i] << " " << lits[i] << " 0\n";
}
out.flush();
}

10
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -115,10 +115,18 @@ public:
if (weights != 0) {
for (unsigned i = 0; i < sz; ++i) m_weights.push_back(weights[i]);
}
init_preprocess();
m_solver.pop_to_base_level();
dep2asm_t dep2asm;
expr_ref_vector asms(m);
for (unsigned i = 0; i < sz; ++i) {
expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
expr_ref fml(m.mk_implies(a, assumptions[i]), m);
assert_expr(fml);
asms.push_back(a);
}
VERIFY(l_true == internalize_formulas());
VERIFY(l_true == internalize_assumptions(sz, assumptions, dep2asm));
VERIFY(l_true == internalize_assumptions(sz, asms.c_ptr(), dep2asm));
svector<unsigned> nweights;
for (unsigned i = 0; i < m_asms.size(); ++i) {
nweights.push_back((unsigned) m_weights[i]);

50
src/sat/tactic/goal2sat.cpp
View file

@ -174,6 +174,7 @@ struct goal2sat::imp {
switch (to_app(t)->get_decl_kind()) {
case OP_NOT:
case OP_OR:
case OP_AND:
case OP_IFF:
m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
return false;
@ -185,7 +186,6 @@ struct goal2sat::imp {
}
convert_atom(t, root, sign);
return true;
case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT: {
@ -215,8 +215,8 @@ struct goal2sat::imp {
}
else {
mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
m_result_stack.reset();
}
m_result_stack.reset();
}
else {
SASSERT(num <= m_result_stack.size());
@ -240,6 +240,48 @@ struct goal2sat::imp {
}
}
void convert_and(app * t, bool root, bool sign) {
TRACE("goal2sat", tout << "convert_and:\n" << mk_ismt2_pp(t, m) << "\n";);
unsigned num = t->get_num_args();
if (root) {
if (sign) {
for (unsigned i = 0; i < num; ++i) {
m_result_stack[i].neg();
}
}
else {
for (unsigned i = 0; i < num; ++i) {
mk_clause(m_result_stack[i]);
}
}
m_result_stack.reset();
}
else {
SASSERT(num <= m_result_stack.size());
sat::bool_var k = m_solver.mk_var();
sat::literal l(k, false);
m_cache.insert(t, l);
// l => /\ lits
sat::literal * lits = m_result_stack.end() - num;
for (unsigned i = 0; i < num; i++) {
mk_clause(~l, lits[i]);
}
// /\ lits => l
for (unsigned i = 0; i < num; ++i) {
m_result_stack[m_result_stack.size() - num + i].neg();
}
m_result_stack.push_back(l);
lits = m_result_stack.end() - num - 1;
mk_clause(num+1, lits);
unsigned old_sz = m_result_stack.size() - num - 1;
m_result_stack.shrink(old_sz);
if (sign)
l.neg();
m_result_stack.push_back(l);
}
}
void convert_ite(app * n, bool root, bool sign) {
unsigned sz = m_result_stack.size();
SASSERT(sz >= 3);
@ -316,6 +358,9 @@ struct goal2sat::imp {
case OP_OR:
convert_or(t, root, sign);
break;
case OP_AND:
convert_and(t, root, sign);
break;
case OP_ITE:
convert_ite(t, root, sign);
break;
@ -456,7 +501,6 @@ struct unsupported_bool_proc {
void operator()(app * n) {
if (n->get_family_id() == m.get_basic_family_id()) {
switch (n->get_decl_kind()) {
case OP_AND:
case OP_XOR:
case OP_IMPLIES:
case OP_DISTINCT: