bddprint.cc 4.53 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2009, 2012, 2014, 2015 Laboratoire de Recherche et
3
4
5
6
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
12
// the Free Software Foundation; either version 3 of the License, or
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
13
14
15
16
17
18
19
20
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
22

23
#include <sstream>
24
#include <cassert>
25
#include <ostream>
26
#include "bddprint.hh"
27
#include "tl/print.hh"
28
#include "formula2bdd.hh"
Thomas Badie's avatar
Thomas Badie committed
29
#include "misc/minato.hh"
30
31
32

namespace spot
{
33
  /// Global dictionary used by print_handler() to lookup variables.
34
  static bdd_dict* dict;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
35

36
37
  /// Global flag to enable Acc[x] output (instead of `x').
  static bool want_acc;
38

39
40
41
42
  /// Global flag to enable UTF-8 output.
  static bool utf8;

  static
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
43
  std::ostream& print_(std::ostream& o, formula f)
44
45
  {
    if (utf8)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
46
      print_utf8_psl(o, f);
47
    else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
48
      print_psl(o, f);
49
50
51
    return o;
  }

52
  /// Stream handler used by Buddy to display BDD variables.
53
  static void
54
  print_handler(std::ostream& o, int v)
55
  {
56
57
58
    assert(unsigned(v) < dict->bdd_map.size());
    const bdd_dict::bdd_info& ref = dict->bdd_map[v];
    switch (ref.type)
59
      {
60
      case bdd_dict::var:
61
	print_(o, ref.f);
62
63
64
	break;
      case bdd_dict::acc:
	if (want_acc)
65
	  {
66
	    o << "Acc[";
67
	    print_(o, ref.f) << ']';
68
69
70
	  }
	else
	  {
71
	    o << '"';
72
	    print_(o, ref.f) << '"';
73
	  }
74
75
	break;
      case bdd_dict::anon:
76
	o << '?' << v;
77
78
79
      }
  }

80

81
82
83
84
85
86
87
88
89
90
  static std::ostream* where;
  static void
  print_sat_handler(char* varset, int size)
  {
    bool not_first = false;
    for (int v = 0; v < size; ++v)
      {
	if (varset[v] < 0)
	  continue;
	if (not_first)
91
	  *where << ' ';
92
93
94
	else
	  not_first = true;
	if (varset[v] == 0)
95
	  *where << "! ";
96
97
98
99
100
	print_handler(*where, v);
      }
  }

  std::ostream&
101
  bdd_print_sat(std::ostream& os, const bdd_dict_ptr& d, bdd b)
102
  {
103
    dict = d.get();
104
    where = &os;
105
106
107
108
109
110
    want_acc = false;
    assert(bdd_satone(b) == b);
    bdd_allsat(b, print_sat_handler);
    return os;
  }

111
112
113
114
115
116
117
118
119
120
121
122
123
124
  static bool first_done = false;
  static void
  print_accset_handler(char* varset, int size)
  {
    for (int v = 0; v < size; ++v)
      if (varset[v] > 0)
	{
	  *where << (first_done ? ", " : "{");
	  print_handler(*where, v);
	  first_done = true;
	}
  }

  std::ostream&
125
  bdd_print_accset(std::ostream& os, const bdd_dict_ptr& d, bdd b)
126
  {
127
    dict = d.get();
128
129
130
131
132
    where = &os;
    want_acc = true;
    first_done = false;
    bdd_allsat(b, print_accset_handler);
    if (first_done)
133
      *where << '}';
134
135
136
    return os;
  }

137
  std::string
138
  bdd_format_accset(const bdd_dict_ptr& d, bdd b)
139
140
141
142
143
144
  {
    std::ostringstream os;
    bdd_print_accset(os, d, b);
    return os.str();
  }

145
  std::string
146
  bdd_format_sat(const bdd_dict_ptr& d, bdd b)
147
148
149
150
151
152
  {
    std::ostringstream os;
    bdd_print_sat(os, d, b);
    return os.str();
  }

153
  std::ostream&
154
  bdd_print_set(std::ostream& os, const bdd_dict_ptr& d, bdd b)
155
  {
156
    dict = d.get();
157
    want_acc = true;
158
159
    bdd_strm_hook(print_handler);
    os << bddset << b;
160
    bdd_strm_hook(nullptr);
161
162
163
    return os;
  }

164
  std::string
165
  bdd_format_set(const bdd_dict_ptr& d, bdd b)
166
167
168
169
170
171
  {
    std::ostringstream os;
    bdd_print_set(os, d, b);
    return os.str();
  }

172
  std::ostream&
173
  bdd_print_formula(std::ostream& os, const bdd_dict_ptr& d, bdd b)
174
  {
175
    return print_(os, bdd_to_formula(b, d));
176
177
178
  }

  std::string
179
  bdd_format_formula(const bdd_dict_ptr& d, bdd b)
180
181
182
183
184
185
  {
    std::ostringstream os;
    bdd_print_formula(os, d, b);
    return os.str();
  }

186
187
188
189
190
  void
  enable_utf8()
  {
    utf8 = true;
  }
Thomas Badie's avatar
Thomas Badie committed
191
192

  std::ostream&
193
  bdd_print_isop(std::ostream& os, const bdd_dict_ptr& d, bdd b)
Thomas Badie's avatar
Thomas Badie committed
194
  {
195
    dict = d.get();
Thomas Badie's avatar
Thomas Badie committed
196
197
198
199
200
201
202
203
204
205
206
207
    want_acc = true;
    minato_isop isop(b);

    bdd p;
    while ((p = isop.next()) != bddfalse)
      {
        os << bdd_format_set(d, p);
      }
    return os;
  }

  std::string
208
  bdd_format_isop(const bdd_dict_ptr& d, bdd b)
Thomas Badie's avatar
Thomas Badie committed
209
210
211
212
213
  {
    std::ostringstream os;
    bdd_print_isop(os, d, b);
    return os.str();
  }
214
}