multop.cc 1.42 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
    multop::multop(type op, formula* first, formula* second)
11
      : op_(op)
12
    {
13
14
15
      children_.reserve(2);
      add(first);
      add(second);
16
17
18
    }
    
    void
19
    multop::add(formula* f)
20
    {
21
      // If the formula we add is itself a multop for the same operator,
22
23
24
25
26
27
28
      // 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));
29
	  // that sub-formula is now useless 
30
31
32
33
34
35
	  delete f;
	}
      else
	{
	  children_.push_back(f);
	}
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
    }

    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();
    }

60
    const formula*
61
62
63
64
65
    multop::nth(unsigned n) const
    {
      return children_[n];
    }

66
    formula* 
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
    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;
    }

  }
}