clone.cc 1.22 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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
#include "ltlast/allnodes.hh"
#include "clone.hh"

namespace spot 
{
  namespace ltl
  {
    clone_visitor::clone_visitor()
    {
    }

    clone_visitor::~clone_visitor()
    {
    }

    formula*
    clone_visitor::result() const
    {
      return result_;
    }
    
    void 
    clone_visitor::visit(const atomic_prop* ap)
    {
      result_ = new atomic_prop(ap->name());
    }

    void 
    clone_visitor::visit(const constant* c)
    {
      result_ = new constant(c->val());
    }

    void 
    clone_visitor::visit(const unop* uo)
    {
      result_ = new unop(uo->op(), recurse(uo->child()));
    }
    
    void 
    clone_visitor::visit(const binop* bo)
    {
      result_ = new binop(bo->op(), 
			  recurse(bo->first()), recurse(bo->second()));
    }
    
    void 
    clone_visitor::visit(const multop* mo)
    {
      multop* res = new multop(mo->op());
      unsigned mos = mo->size();
      for (unsigned i = 0; i < mos; ++i)
	{
	  res->add(recurse(mo->nth(i)));
	}
      result_ = res;
    }

    formula* 
    clone_visitor::recurse(const formula* f)
    {
      return clone(f);
    }

    formula* 
    clone(const formula* f)
    {
      clone_visitor v;
      f->accept(v);
      return v.result();
    }

  }
}