bddprint.cc 3.19 KB
Newer Older
1
#include <sstream>
2
#include <cassert>
3
4
5
6
7
#include "bddprint.hh"
#include "ltlvisit/tostring.hh"

namespace spot
{
8
  /// Global dictionary used by print_handler() to lookup variables.
9
  static const tgba_bdd_dict* dict;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
10

11
12
  /// Global flag to enable Acc[x] output (instead of `x').
  static bool want_acc;
13

14
  /// Stream handler used by Buddy to display BDD variables.
15
16
17
  static void
  print_handler(std::ostream& o, int var)
  {
18
    tgba_bdd_dict::vf_map::const_iterator isi =
19
20
21
22
23
      dict->var_formula_map.find(var);
    if (isi != dict->var_formula_map.end())
      to_string(isi->second, o);
    else
      {
24
25
	isi = dict->acc_formula_map.find(var);
	if (isi != dict->acc_formula_map.end())
26
	  {
27
	    if (want_acc)
28
	      {
29
		o << "Acc[";
30
31
32
33
34
35
36
		to_string(isi->second, o) << "]";
	      }
	    else
	      {
		o << "\"";
		to_string(isi->second, o) << "\"";
	      }
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
	  }
	else
	  {
	    isi = dict->now_formula_map.find(var);
	    if (isi != dict->now_formula_map.end())
	      {
		o << "Now["; to_string(isi->second, o) << "]";
	      }
	    else
	      {
		isi = dict->now_formula_map.find(var - 1);
		if (isi != dict->now_formula_map.end())
		  {
		    o << "Next["; to_string(isi->second, o) << "]";
		  }
		else
		  {
		    o << "?" << var;
		  }
	      }
	  }
      }
  }

61

62
63
64
65
66
67
68
69
70
71
72
73
74
75
  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)
	  *where << " ";
	else
	  not_first = true;
	if (varset[v] == 0)
76
77
	  // The space is important for LBTT.
	  *where << "! ";
78
79
80
81
82
83
84
85
86
	print_handler(*where, v);
      }
  }

  std::ostream&
  bdd_print_sat(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
    where = &os;
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
    want_acc = false;
    assert(bdd_satone(b) == b);
    bdd_allsat(b, print_sat_handler);
    return os;
  }

  static void
  print_acc_handler(char* varset, int size)
  {
    for (int v = 0; v < size; ++v)
      {
	if (varset[v] < 0)
	  continue;
	if (varset[v] > 0)
	  {
	    *where << " ";
	    print_handler(*where, v);
	  }
      }
  }

  std::ostream&
  bdd_print_acc(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
    where = &os;
    want_acc = false;
    bdd_allsat(b, print_acc_handler);
115
116
117
118
119
120
121
122
123
124
125
    return os;
  }

  std::string
  bdd_format_sat(const tgba_bdd_dict& d, bdd b)
  {
    std::ostringstream os;
    bdd_print_sat(os, d, b);
    return os.str();
  }

126
  std::ostream&
127
128
129
  bdd_print_set(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
130
    want_acc = true;
131
132
133
134
135
136
    bdd_strm_hook(print_handler);
    os << bddset << b;
    bdd_strm_hook(0);
    return os;
  }

137
138
139
140
141
142
143
144
145
  std::string
  bdd_format_set(const tgba_bdd_dict& d, bdd b)
  {
    std::ostringstream os;
    bdd_print_set(os, d, b);
    return os.str();
  }

  std::ostream&
146
147
148
  bdd_print_dot(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
149
    want_acc = true;
150
151
152
153
154
    bdd_strm_hook(print_handler);
    os << bdddot << b;
    bdd_strm_hook(0);
    return os;
  }
155
156

  std::ostream&
157
158
159
  bdd_print_table(std::ostream& os, const tgba_bdd_dict& d, bdd b)
  {
    dict = &d;
160
    want_acc = true;
161
162
163
164
165
166
167
    bdd_strm_hook(print_handler);
    os << bddtable << b;
    bdd_strm_hook(0);
    return os;
  }

}