multop.cc 2.52 KB
Newer Older
1
2
3
4
5
6
7
8
#include <cassert>
#include <utility>
#include "multop.hh"
#include "visitor.hh"

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

15
16
    multop::~multop()
    {
17
18
19
20
21
22
      // 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);

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

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

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

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

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

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

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

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

77
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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
    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);
    }

    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)
	    v->push_back(p->nth(i));
	  // that sub-formula is now useless
	  formula::unref(f);
	}
      else
	{
	  v->push_back(f);
	}
      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);
    }

141
142
143
144
145
    unsigned
    multop::instance_count()
    {
      return instances.size();
    }
146
147
  }
}