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

namespace spot
{
  namespace ltl
  {    
    multop::multop(type op, formulae* first, formulae* second)
11
      : op_(op)
12
    {
13
14
15
      children_.reserve(2);
      add(first);
      add(second);
16
17
18
19
20
    }
    
    void
    multop::add(formulae* f)
    {
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
      // If the formulae we add is itself a multop for the same operator,
      // 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));
	  // that sub-formulae is now useless 
	  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
60
61
62
63
64
65
66
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::~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();
    }

    const formulae*
    multop::nth(unsigned n) const
    {
      return children_[n];
    }

    formulae* 
    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;
    }

  }
}