mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

adding facility to dump wcnf benchmarks

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-21 07:26:49 -07:00
parent 954e612188
commit a78fc031bc
5 changed files with 88 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

44
src/sat/sat_solver.cpp
View file

@ -2616,6 +2616,50 @@ namespace sat {
}
}
void solver::display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const {
unsigned max_weight = 0;
for (unsigned i = 0; i < sz; ++i) {
max_weight = std::max(max_weight, weights[i]);
}
++max_weight;
out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
for (unsigned i = 0; i < m_trail.size(); i++) {
out << dimacs_lit(m_trail[i]) << " 0\n";
}
vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l = ~to_literal(l_idx);
watch_list const & wlist = *it;
watch_list::const_iterator it2 = wlist.begin();
watch_list::const_iterator end2 = wlist.end();
for (; it2 != end2; ++it2) {
if (it2->is_binary_clause() && l.index() < it2->get_literal().index())
out << max_weight << " " << dimacs_lit(l) << " " << dimacs_lit(it2->get_literal()) << " 0\n";
}
}
clause_vector const * vs[2] = { &m_clauses, &m_learned };
for (unsigned i = 0; i < 2; i++) {
clause_vector const & cs = *(vs[i]);
clause_vector::const_iterator it = cs.begin();
clause_vector::const_iterator end = cs.end();
for (; it != end; ++it) {
clause const & c = *(*it);
unsigned sz = c.size();
out << max_weight << " ";
for (unsigned j = 0; j < sz; j++)
out << dimacs_lit(c[j]) << " ";
out << "0\n";
}
}
for (unsigned i = 0; i < sz; ++i) {
out << weights[i] << " " << lits[i] << " 0\n";
}
}
void solver::display_watches(std::ostream & out) const {
vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end();

1
src/sat/sat_solver.h
View file

@ -447,6 +447,7 @@ namespace sat {
void display(std::ostream & out) const;
void display_watches(std::ostream & out) const;
void display_dimacs(std::ostream & out) const;
void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
void display_assignment(std::ostream & out) const;
void display_justification(std::ostream & out, justification const& j) const;

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

@ -98,28 +98,36 @@ public:
virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
return check_sat(num_assumptions, assumptions, 0, 0);
}
void display_weighted(std::ostream& out, unsigned sz, expr * const * assumptions, unsigned const* weights) {
m_solver.pop_to_base_level();
dep2asm_t dep2asm;
VERIFY(l_true == internalize_formulas());
VERIFY(l_true == internalize_assumptions(sz, assumptions, 0 != weights, dep2asm));
m_solver.display_wcnf(out, sz, m_asms.c_ptr(), weights);
}
lbool check_sat(unsigned num_assumptions, expr * const * assumptions, double const* weights, double max_weight) {
lbool check_sat(unsigned sz, expr * const * assumptions, double const* weights, double max_weight) {
m_solver.pop_to_base_level();
dep2asm_t dep2asm;
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(num_assumptions, assumptions, weights, dep2asm);
r = internalize_assumptions(sz, assumptions, 0 != weights, dep2asm);
if (r != l_true) return r;
//m_solver.display_dimacs(std::cout);
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), weights, max_weight);
switch (r) {
case l_true:
if (num_assumptions > 0 && !weights) {
if (sz > 0 && !weights) {
check_assumptions(dep2asm);
}
break;
case l_false:
// TBD: expr_dependency core is not accounted for.
if (num_assumptions > 0) {
if (sz > 0) {
extract_core(dep2asm);
}
break;
@ -251,12 +259,12 @@ private:
return l_true;
}
lbool internalize_assumptions(unsigned sz, expr* const* asms, double const* weights, dep2asm_t& dep2asm) {
lbool internalize_assumptions(unsigned sz, expr* const* asms, bool is_weighted, dep2asm_t& dep2asm) {
if (sz == 0) {
return l_true;
}
if (weights) {
return internalize_weighted(sz, asms, weights, dep2asm);
if (is_weighted) {
return internalize_weighted(sz, asms, dep2asm);
}
return internalize_unweighted(sz, asms, dep2asm);
}
@ -278,7 +286,7 @@ private:
\brief extract weighted assumption literals in the same order as the weights.
For this purpose we enforce tha assumptions are literals.
*/
lbool internalize_weighted(unsigned sz, expr* const* asms, double const* weights, dep2asm_t& dep2asm) {
lbool internalize_weighted(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
goal_ref g = alloc(goal, m, true, true); // models and cores are enabled.
lbool res = l_undef;
m_asms.reset();
@ -441,3 +449,15 @@ lbool inc_sat_check_sat(solver& _s, unsigned sz, expr*const* soft, rational cons
}
return s.check_sat(sz, soft, weights.c_ptr(), max_weight.get_double());
}
void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* soft, rational const* _weights) {
inc_sat_solver& s = dynamic_cast<inc_sat_solver&>(_s);
vector<unsigned> weights;
for (unsigned i = 0; _weights && i < sz; ++i) {
if (!_weights[i].is_unsigned()) {
throw default_exception("Cannot display weights that are not integers");
}
weights.push_back(_weights[i].get_unsigned());
}
return s.display_weighted(out, sz, soft, weights.c_ptr());
}

2
src/sat/sat_solver/inc_sat_solver.h
View file

@ -26,4 +26,6 @@ solver* mk_inc_sat_solver(ast_manager& m, params_ref const& p);
lbool inc_sat_check_sat(solver& s, unsigned sz, expr*const* soft, rational const* weights, rational const& max_weight);
void inc_sat_display(std::ostream& out, solver& s, unsigned sz, expr*const* soft, rational const* _weights);
#endif