enable wcnf output for weighted maxsat problems

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;
 }

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);
 

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 {

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(); }

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'),

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);