1 /*++
2 Copyright (c) 2019 Microsoft Corporation
3 
4 Module Name:
5 
6     display_dimacs.h
7 
8 Abstract:
9 
10     Display expressions in DIMACS format.
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner0 2019-01-24
15 
16 Revision History:
17 
18 --*/
19 
20 #include "ast.h"
21 #include "display_dimacs.h"
22 
23 struct dimacs_pp {
24     ast_manager& m;
25     unsigned_vector expr2var;
26     ptr_vector<expr> exprs;
27     unsigned num_vars { 0 };
28 
dimacs_ppdimacs_pp29     dimacs_pp(ast_manager& m): m(m) {}
30 
resetdimacs_pp31     void reset() {
32         num_vars = 0;
33         expr2var.reset();
34         exprs.reset();
35     }
36 
init_from_dimacsdimacs_pp37     bool init_from_dimacs(expr* f) {
38         unsigned num_lits;
39         expr * const * lits;
40         if (m.is_or(f)) {
41             num_lits = to_app(f)->get_num_args();
42             lits     = to_app(f)->get_args();
43         }
44         else {
45             num_lits = 1;
46             lits     = &f;
47         }
48         for (unsigned j = 0; j < num_lits; j++) {
49             expr * l = lits[j];
50             if (m.is_not(l))
51                 l = to_app(l)->get_arg(0);
52             if (!is_uninterp_const(l))
53                 return false;
54             symbol const& s = to_app(l)->get_decl()->get_name();
55             if (s.is_numerical() && s.get_num() > 0) {
56                 if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
57                     ++num_vars;
58                     expr2var.setx(l->get_id(), s.get_num(), UINT_MAX);
59                     exprs.setx(l->get_id(), l, nullptr);
60                 }
61                 continue;
62             }
63             return false;
64         }
65         return true;
66     }
67 
init_formuladimacs_pp68     void init_formula(expr* f) {
69         unsigned num_lits;
70         expr * const * lits;
71         if (m.is_or(f)) {
72             num_lits = to_app(f)->get_num_args();
73             lits     = to_app(f)->get_args();
74         }
75         else {
76             num_lits = 1;
77             lits     = &f;
78         }
79         for (unsigned j = 0; j < num_lits; j++) {
80             expr * l = lits[j];
81             if (m.is_not(l))
82                 l = to_app(l)->get_arg(0);
83             if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
84                 num_vars++;
85                 expr2var.setx(l->get_id(), num_vars, UINT_MAX);
86                 exprs.setx(l->get_id(), l, nullptr);
87             }
88         }
89     }
90 
pp_formuladimacs_pp91     void pp_formula(std::ostream& out, expr* f) {
92         unsigned num_lits;
93         expr * const * lits;
94         if (m.is_or(f)) {
95             num_lits = to_app(f)->get_num_args();
96             lits     = to_app(f)->get_args();
97         }
98         else {
99             num_lits = 1;
100             lits     = &f;
101         }
102         for (unsigned j = 0; j < num_lits; j++) {
103             expr * l = lits[j];
104             if (m.is_not(l)) {
105                 out << "-";
106                 l = to_app(l)->get_arg(0);
107             }
108             SASSERT(exprs[l->get_id()]);
109             out << expr2var[l->get_id()] << " ";
110         }
111         out << "0\n";
112     }
113 
pp_defsdimacs_pp114     void pp_defs(std::ostream& out) {
115         for (expr* e : exprs)
116             if (e && is_app(e)) {
117                 symbol const& n = to_app(e)->get_decl()->get_name();
118                 out << "c " << expr2var[e->get_id()] << " " << n << "\n";
119             }
120     }
121 
122 };
123 
display_dimacs(std::ostream & out,expr_ref_vector const & fmls,bool include_names)124 std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls, bool include_names) {
125     ast_manager& m = fmls.m();
126     dimacs_pp pp(m);
127     unsigned num_cls  = fmls.size();
128     bool is_from_dimacs = true;
129     for (expr * f : fmls) {
130         is_from_dimacs = pp.init_from_dimacs(f);
131         if (!is_from_dimacs)
132             break;
133     }
134 
135     if (!is_from_dimacs) {
136         pp.reset();
137         for (expr * f : fmls) {
138             pp.init_formula(f);
139         }
140     }
141     out << "p cnf " << pp.num_vars << " " << num_cls << "\n";
142     for (expr* f : fmls)
143         pp.pp_formula(out, f);
144     if (include_names && !is_from_dimacs)
145         pp.pp_defs(out);
146     return out;
147 }
148 
display_wcnf(std::ostream & out,expr_ref_vector const & fmls,svector<std::pair<expr *,unsigned>> const & soft)149 std::ostream& display_wcnf(std::ostream& out, expr_ref_vector const& fmls, svector<std::pair<expr*,unsigned>> const& soft) {
150     ast_manager& m = fmls.m();
151     dimacs_pp pp(m);
152     for (expr* f : fmls)
153         pp.init_formula(f);
154     for (auto s : soft)
155         pp.init_formula(s.first);
156     out << "p wcnf " << pp.num_vars << " " << fmls.size() + soft.size() << "\n";
157     unsigned sum_soft = 1;
158     for (auto s : soft)
159         sum_soft += s.second;
160     for (expr* f : fmls) {
161         out << sum_soft << " ";
162         pp.pp_formula(out, f);
163     }
164     for (auto s : soft) {
165         out << s.second << " ";
166         pp.pp_formula(out, s.first);
167     }
168     pp.pp_defs(out);
169     return out;
170 }
171