diff --git a/src/ast/display_dimacs.cpp b/src/ast/display_dimacs.cpp
index 50a1ff6d0..6b2ef6658 100644
--- a/src/ast/display_dimacs.cpp
+++ b/src/ast/display_dimacs.cpp
@@ -20,14 +20,21 @@ Revision History:
#include "ast.h"
#include "display_dimacs.h"
-std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names) {
- ast_manager& m = fmls.m();
+struct dimacs_pp {
+ ast_manager& m;
unsigned_vector expr2var;
ptr_vector<expr> exprs;
- unsigned num_vars = 0;
- unsigned num_cls = fmls.size();
- bool is_from_dimacs = true;
- for (expr * f : fmls) {
+ unsigned num_vars { 0 };
+
+ dimacs_pp(ast_manager& m): m(m) {}
+
+ void reset() {
+ num_vars = 0;
+ expr2var.reset();
+ exprs.reset();
+ }
+
+ bool init_from_dimacs(expr* f) {
unsigned num_lits;
expr * const * lits;
if (m.is_or(f)) {
@@ -42,10 +49,8 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, boo
expr * l = lits[j];
if (m.is_not(l))
l = to_app(l)->get_arg(0);
- if (!is_uninterp_const(l)) {
- is_from_dimacs = false;
- break;
- }
+ if (!is_uninterp_const(l))
+ return false;
symbol const& s = to_app(l)->get_decl()->get_name();
if (s.is_numerical() && s.get_num() > 0) {
if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
@@ -55,43 +60,35 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, boo
}
continue;
}
- is_from_dimacs = false;
- break;
+ return false;
}
- if (!is_from_dimacs) {
- num_vars = 0;
- expr2var.reset();
- exprs.reset();
- break;
+ return true;
+ }
+
+ void init_formula(expr* f) {
+ unsigned num_lits;
+ expr * const * lits;
+ if (m.is_or(f)) {
+ num_lits = to_app(f)->get_num_args();
+ lits = to_app(f)->get_args();
}
- }
-
- if (!is_from_dimacs) {
- for (expr * f : fmls) {
- unsigned num_lits;
- expr * const * lits;
- if (m.is_or(f)) {
- num_lits = to_app(f)->get_num_args();
- lits = to_app(f)->get_args();
- }
- else {
- num_lits = 1;
- lits = &f;
- }
- for (unsigned j = 0; j < num_lits; j++) {
- expr * l = lits[j];
- if (m.is_not(l))
- l = to_app(l)->get_arg(0);
- if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
- num_vars++;
- expr2var.setx(l->get_id(), num_vars, UINT_MAX);
- exprs.setx(l->get_id(), l, nullptr);
- }
+ else {
+ num_lits = 1;
+ lits = &f;
+ }
+ for (unsigned j = 0; j < num_lits; j++) {
+ expr * l = lits[j];
+ if (m.is_not(l))
+ l = to_app(l)->get_arg(0);
+ if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
+ num_vars++;
+ expr2var.setx(l->get_id(), num_vars, UINT_MAX);
+ exprs.setx(l->get_id(), l, nullptr);
}
}
}
- out << "p cnf " << num_vars << " " << num_cls << "\n";
- for (expr* f : fmls) {
+
+ void pp_formula(std::ostream& out, expr* f) {
unsigned num_lits;
expr * const * lits;
if (m.is_or(f)) {
@@ -113,18 +110,61 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, boo
}
out << "0\n";
}
- if (include_names && !is_from_dimacs) {
- for (expr* e : exprs) {
+
+ void pp_defs(std::ostream& out) {
+ for (expr* e : exprs)
if (e && is_app(e)) {
symbol const& n = to_app(e)->get_decl()->get_name();
out << "c " << expr2var[e->get_id()] << " " << n << "\n";
}
+ }
+
+};
+
+std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names) {
+ ast_manager& m = fmls.m();
+ dimacs_pp pp(m);
+ unsigned num_cls = fmls.size();
+ bool is_from_dimacs = true;
+ for (expr * f : fmls) {
+ is_from_dimacs = pp.init_from_dimacs(f);
+ if (!is_from_dimacs)
+ break;
+ }
+
+ if (!is_from_dimacs) {
+ pp.reset();
+ for (expr * f : fmls) {
+ pp.init_formula(f);
}
}
+ out << "p cnf " << pp.num_vars << " " << num_cls << "\n";
+ for (expr* f : fmls)
+ pp.pp_formula(out, f);
+ if (include_names && !is_from_dimacs)
+ pp.pp_defs(out);
return out;
}
-std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, vector<std::pair<expr*,unsigned>> const& soft, bool include_names) {
- NOT_IMPLEMENTED_YET();
+std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, svector<std::pair<expr*,unsigned>> const& soft) {
+ ast_manager& m = fmls.m();
+ dimacs_pp pp(m);
+ for (expr* f : fmls)
+ pp.init_formula(f);
+ for (auto s : soft)
+ pp.init_formula(s.first);
+ out << "p wcnf " << pp.num_vars << " " << fmls.size() + soft.size() << "\n";
+ unsigned sum_soft = 1;
+ for (auto s : soft)
+ sum_soft += s.second;
+ for (expr* f : fmls) {
+ out << sum_soft << " ";
+ pp.pp_formula(out, f);
+ }
+ for (auto s : soft) {
+ out << s.second << " ";
+ pp.pp_formula(out, s.first);
+ }
+ pp.pp_defs(out);
return out;
}
diff --git a/src/ast/display_dimacs.h b/src/ast/display_dimacs.h
index a50684682..0af4dc4a0 100644
--- a/src/ast/display_dimacs.h
+++ b/src/ast/display_dimacs.h
@@ -22,5 +22,5 @@ Revision History:
std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names);
-std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, vector<std::pair<expr*,unsigned>> const& soft, bool include_names);
+std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, svector<std::pair<expr*,unsigned>> const& soft);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 2307c2488..429b537b9 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -24,6 +24,7 @@ Notes:
#include "ast/pb_decl_plugin.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_pp_util.h"
+#include "ast/display_dimacs.h"
#include "model/model_smt2_pp.h"
#include "tactic/goal.h"
#include "tactic/tactic.h"
@@ -1540,9 +1541,12 @@ namespace opt {
m_enable_sls = _p.enable_sls();
m_maxsat_engine = _p.maxsat_engine();
m_pp_neat = _p.pp_neat();
+ m_pp_wcnf = _p.pp_wcnf();
}
- std::string context::to_string() const {
+ std::string context::to_string() {
+ if (m_pp_wcnf)
+ return to_wcnf();
return to_string(false, m_scoped_state.m_hard, m_scoped_state.m_objectives);
}
@@ -1557,6 +1561,9 @@ namespace opt {
auto const& objectives = m_objectives;
if (objectives.size() > 1)
throw default_exception("only single objective weighted MaxSAT wcnf output is supported");
+ ptr_vector<expr> soft_f;
+ vector<rational> soft_w;
+ svector<std::pair<expr*, unsigned>> soft;
if (objectives.size() == 1) {
auto const& obj = objectives[0];
if (obj.m_type != O_MAXSMT)
@@ -1565,10 +1572,15 @@ namespace opt {
rational w = obj.m_weights[j];
if (!w.is_unsigned())
throw default_exception("only single objective weighted MaxSAT wcnf output is supported");
+ soft_f.push_back(obj.m_terms[j]);
+ soft_w.push_back(w);
}
}
- NOT_IMPLEMENTED_YET();
- return std::string("");
+ std::ostringstream strm;
+ m_sat_solver = mk_inc_sat_solver(m, m_params);
+ m_sat_solver->assert_expr(m_hard_constraints);
+ inc_sat_display(strm, *m_sat_solver.get(), soft_f.size(), soft_f.c_ptr(), soft_w.c_ptr());
+ return strm.str();
}
std::string context::to_string(bool is_internal, expr_ref_vector const& hard, vector<objective> const& objectives) const {
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 8a6df7129..28cff40d3 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -179,10 +179,11 @@ namespace opt {
func_decl_ref_vector m_objective_refs;
expr_ref_vector m_core;
tactic_ref m_simplify;
- bool m_enable_sat;
- bool m_enable_sls;
- bool m_is_clausal;
- bool m_pp_neat;
+ bool m_enable_sat { true } ;
+ bool m_enable_sls { false };
+ bool m_is_clausal { false };
+ bool m_pp_neat { true };
+ bool m_pp_wcnf { false };
symbol m_maxsat_engine;
symbol m_logic;
svector<symbol> m_labels;
@@ -232,7 +233,7 @@ namespace opt {
void get_lower(unsigned idx, expr_ref_vector& es) { to_exprs(get_lower_as_num(idx), es); }
void get_upper(unsigned idx, expr_ref_vector& es) { to_exprs(get_upper_as_num(idx), es); }
- std::string to_string() const;
+ std::string to_string();
unsigned num_objectives() override { return m_scoped_state.m_objectives.size(); }
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 2192ed9ce..5106c5492 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -16,6 +16,7 @@ def_module_params('opt',
('elim_01', BOOL, True, 'eliminate 01 variables'),
('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
+ ('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'),
('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index b156e6694..301140eb1 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -4002,17 +4002,18 @@ 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]);
- }
+ for (unsigned i = 0; i < sz; ++i)
+ max_weight += weights[i];
++max_weight;
+ if (m_ext)
+ throw default_exception("wcnf is only supported for pure CNF problems");
+
out << "p wcnf " << num_vars() << " " << num_clauses() + sz << " " << max_weight << "\n";
out << "c soft " << sz << "\n";
- for (literal lit : m_trail) {
+ for (literal lit : m_trail)
out << max_weight << " " << dimacs_lit(lit) << " 0\n";
- }
unsigned l_idx = 0;
for (watch_list const& wlist : m_watches) {
literal l = ~to_literal(l_idx);