formula2bdd.cc 4.07 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2009-2017 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
5
6
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
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
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/>.
22

23
#include <cassert>
24
25
#include <spot/twa/formula2bdd.hh>
#include <spot/misc/minato.hh>
26
27
28

namespace spot
{
29
  namespace
30
  {
31
    // Convert a BDD which is known to be a conjonction into a formula.
32
    static formula
33
    conj_to_formula(bdd b, const bdd_dict_ptr d)
34
    {
35
      if (b == bddfalse)
36
        return formula::ff();
37
      std::vector<formula> v;
38
      while (b != bddtrue)
39
40
41
        {
          int var = bdd_var(b);
          const bdd_dict::bdd_info& i = d->bdd_map[var];
42
43
44
45
          if (SPOT_UNLIKELY(i.type != bdd_dict::var))
            throw std::runtime_error("bdd_to_formula() was passed a bdd"
                                     " with a variable that is not in "
                                     "the dictionary");
46
          formula res = i.f;
47

48
49
50
51
52
53
54
55
56
57
58
59
60
          bdd high = bdd_high(b);
          if (high == bddfalse)
            {
              res = formula::Not(res);
              b = bdd_low(b);
            }
          else
            {
              // If bdd_low is not false, then b was not a conjunction.
              assert(bdd_low(b) == bddfalse);
              b = high;
            }
          assert(b != bddfalse);
61
          v.emplace_back(res);
62
        }
63
      return formula::And(v);
64
    }
65
  } // anonymous
66
67

  bdd
68
  formula_to_bdd(formula f, const bdd_dict_ptr& d, void* owner)
69
  {
70
71
    auto recurse = [&d, owner](formula f)
      {
72
        return formula_to_bdd(f, d, owner);
73
74
75
      };
    switch (f.kind())
      {
76
      case op::ff:
77
        return bddfalse;
78
      case op::tt:
79
        return bddtrue;
80
      case op::eword:
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
      case op::Star:
      case op::FStar:
      case op::F:
      case op::G:
      case op::X:
      case op::Closure:
      case op::NegClosure:
      case op::NegClosureMarked:
      case op::U:
      case op::R:
      case op::W:
      case op::M:
      case op::UConcat:
      case op::EConcat:
      case op::EConcatMarked:
      case op::Concat:
      case op::Fusion:
      case op::AndNLM:
      case op::OrRat:
      case op::AndRat:
101
        SPOT_UNIMPLEMENTED();
102
      case op::ap:
103
        return bdd_ithvar(d->register_proposition(f, owner));
104
      case op::Not:
105
        return bdd_not(recurse(f[0]));
106
      case op::Xor:
107
        return bdd_apply(recurse(f[0]), recurse(f[1]), bddop_xor);
108
      case op::Implies:
109
        return bdd_apply(recurse(f[0]), recurse(f[1]), bddop_imp);
110
      case op::Equiv:
111
        return bdd_apply(recurse(f[0]), recurse(f[1]), bddop_biimp);
112
113
      case op::And:
      case op::Or:
114
115
116
117
118
119
120
121
122
123
124
125
126
        {
          int o = bddop_and;
          bdd res = bddtrue;
          if (f.is(op::Or))
            {
              o = bddop_or;
              res = bddfalse;
            }
          unsigned s = f.size();
          for (unsigned n = 0; n < s; ++n)
            res = bdd_apply(res, recurse(f[n]), o);
          return res;
        }
127
128
129
      }
    SPOT_UNREACHABLE();
    return bddfalse;
130
131
  }

132
  formula
133
  bdd_to_formula(bdd f, const bdd_dict_ptr d)
134
135
  {
    if (f == bddfalse)
136
      return formula::ff();
137

138
    std::vector<formula> v;
139
140
141
142

    minato_isop isop(f);
    bdd cube;
    while ((cube = isop.next()) != bddfalse)
143
144
      v.emplace_back(conj_to_formula(cube, d));
    return formula::Or(std::move(v));
145
146
  }
}