multop.cc 3.16 KB
Newer Older
1
2
3
4
#include <cassert>
#include <utility>
#include "multop.hh"
#include "visitor.hh"
5
#include "ltlvisit/destroy.hh"
6
7
8
9

namespace spot
{
  namespace ltl
10
11
12
  {
    multop::multop(type op, vec* v)
      : op_(op), children_(v)
13
14
15
    {
    }

16
17
    multop::~multop()
    {
18
19
20
21
22
23
      // Get this instance out of the instance map.
      pair p(op(), children_);
      map::iterator i = instances.find(p);
      assert (i != instances.end());
      instances.erase(i);

24
      delete children_;
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
    }

    void
    multop::accept(visitor& v)
    {
      v.visit(this);
    }

    void
    multop::accept(const_visitor& v) const
    {
      v.visit(this);
    }

    unsigned
    multop::size() const
    {
42
      return children_->size();
43
44
    }

45
    const formula*
46
47
    multop::nth(unsigned n) const
    {
48
      return (*children_)[n];
49
50
    }

51
    formula*
52
53
    multop::nth(unsigned n)
    {
54
      return (*children_)[n];
55
56
    }

57
    multop::type
58
59
60
61
62
    multop::op() const
    {
      return op_;
    }

63
    const char*
64
65
66
67
68
69
70
71
72
73
74
75
76
77
    multop::op_name() const
    {
      switch (op_)
	{
	case And:
	  return "And";
	case Or:
	  return "Or";
	}
      // Unreachable code.
      assert(0);
      return 0;
    }

78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
    multop::map multop::instances;

    multop*
    multop::instance(type op, vec* v)
    {
      pair p(op, v);
      map::iterator i = instances.find(p);
      if (i != instances.end())
	{
	  delete v;
	  return static_cast<multop*>(i->second->ref());
	}
      multop* ap = new multop(op, v);
      instances[p] = ap;
      return static_cast<multop*>(ap->ref());

    }

    multop*
    multop::instance(type op)
    {
      return instance(op, new vec);
    }

    multop*
    multop::instance(type op, formula* first, formula* second)
    {
      vec* v = new vec;
      multop::add(op, v, first);
      multop::add(op, v, second);
      return instance(op, v);
    }

111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
    void
    multop::add_sorted(vec* v, formula* f)
    {
      // Keep V sorted.  When adding a new multop, iterate over all
      // element until we find either an identicalle element, or the
      // place where the new one should be inserted.
      vec::iterator i;
      for (i = v->begin(); i != v->end(); ++i)
	{
	  if (*i > f)
	    break;
	  if (*i == f)
	    {
	      // F is arleady a child.  Drop it.
	      destroy(f);
	      return;
	    }
	}
      v->insert(i, f);
    }

132
133
134
135
136
137
138
139
140
141
    multop::vec*
    multop::add(type op, vec* v, formula* f)
    {
      // If the formula we add is itself a multop for the same operator,
      // merge its children.
      multop* p = dynamic_cast<multop*>(f);
      if (p && p->op() == op)
	{
	  unsigned ps = p->size();
	  for (unsigned i = 0; i < ps; ++i)
142
143
144
145
	    add_sorted(v, p->nth(i));
	  // That sub-formula is now useless, drop it.
	  // Note that we use unref(), not destroy(), because we've
	  // adopted its children and don't want to destroy these.
146
147
148
149
	  formula::unref(f);
	}
      else
	{
150
	  add_sorted(v, f);
151
152
153
154
155
156
157
158
159
160
161
162
163
164
	}
      return v;
    }

    void
    multop::add(multop** m, formula* f)
    {
      vec* v = new vec(*(*m)->children_);
      type op = (*m)->op();
      multop::add(op, v, f);
      formula::unref(*m);
      *m = instance(op, v);
    }

165
166
167
168
169
    unsigned
    multop::instance_count()
    {
      return instances.size();
    }
170
171
  }
}