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

namespace spot
{
  namespace ltl
  {    
10
11
12
13
14
    multop::multop(type op)
      : op_(op)
    {
    }

15
    multop::multop(type op, formula* first, formula* second)
16
      : op_(op)
17
    {
18
19
20
      children_.reserve(2);
      add(first);
      add(second);
21
22
23
    }
    
    void
24
    multop::add(formula* f)
25
    {
26
      // If the formula we add is itself a multop for the same operator,
27
28
29
30
31
32
33
      // merge its children with ours.
      multop* p = dynamic_cast<multop*>(f);
      if (p && p->op() == op())
	{
	  unsigned ps = p->size();
	  for (unsigned i = 0; i < ps; ++i)
	    children_.push_back(p->nth(i));
34
	  // that sub-formula is now useless 
35
36
37
38
39
40
	  delete f;
	}
      else
	{
	  children_.push_back(f);
	}
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
    }

    multop::~multop()
    {
    }

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

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

    unsigned
    multop::size() const
    {
      return children_.size();
    }

65
    const formula*
66
67
68
69
70
    multop::nth(unsigned n) const
    {
      return children_[n];
    }

71
    formula* 
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
    multop::nth(unsigned n)
    {
      return children_[n];
    }

    multop::type 
    multop::op() const
    {
      return op_;
    }

    const char* 
    multop::op_name() const
    {
      switch (op_)
	{
	case And:
	  return "And";
	case Or:
	  return "Or";
	}
      // Unreachable code.
      assert(0);
      return 0;
    }

  }
}