equals.cc 3.24 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
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
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
#include <vector>
#include "equals.hh"
#include "ltlast/allnodes.hh"

namespace spot 
{
  namespace ltl
  {
    equals_visitor::equals_visitor(const formulae* f)
      : f_(f), result_(false)
    {
    }

    equals_visitor::~equals_visitor()
    {
    }

    bool 
    equals_visitor::result() const
    {
      return result_;
    }
      
    void
    equals_visitor::visit(const atomic_prop* ap)
    {
      const atomic_prop* p = dynamic_cast<const atomic_prop*>(f_);
      if (p && p->name() == ap->name())
	result_ = true;
    }

    void
    equals_visitor::visit(const constant* c)
    {
      const constant* p = dynamic_cast<const constant*>(f_);
      if (p && p->val() == c->val())
	result_ = true;
    }

    void
    equals_visitor::visit(const unop* uo)
    {
      const unop* p = dynamic_cast<const unop*>(f_);
      if (!p || p->op() != uo->op())
	return;
      f_ = p->child();
      uo->child()->accept(*this);
    }

    void
    equals_visitor::visit(const binop* bo)
    {
      const binop* p = dynamic_cast<const binop*>(f_);
      if (!p || p->op() != bo->op())
	return;
      
      // The current visitor will descend the left branch.
      // Build a second visitor for the right branch.
      equals_visitor v2(p->second());
      f_ = p->first();
      
      bo->first()->accept(*this);
      if (result_ == false)
	return;
      
      bo->second()->accept(v2);
      result_ = v2.result();
    }
    
    void
    equals_visitor::visit(const multop* m)
    {
      const multop* p = dynamic_cast<const multop*>(f_);
      if (!p || p->op() != m->op())
	return;
      
      // This check is a bit more complicated than other checks
      // because And(a, b, c) is equal to And(c, a, b, a).
      
      unsigned m_size = m->size();
      unsigned p_size = p->size();
      std::vector<bool> p_seen(p_size, false);
      
      for (unsigned nf = 0; nf < m_size; ++nf)
	{
	  unsigned np;
	  const formulae* mnth = m->nth(nf);
	  for (np = 0; np < p_size; ++np)
	    {
	      if (equals(p->nth(np), mnth))
		{
		  p_seen[np] = true;
		  break;
		}
	    }
	  // We we haven't found mnth in any child of p, then
	  // the two formulaes aren't equal.
	  if (np == p_size)
	    return;
	}
      // At this point, we have found all children of m' in children
      // of `p'.  That doesn't means that both formula are equal.
      // Condider m = And(a, b, c) against p = And(c, d, a, b).
      // We should now check if any unmarked (accodring to p_seen)
      // child of `p' has an counterpart in `m'.  Because `m' might 
      // contain duplicate children, its faster to test that
      // unmarked children of `p' have a counterpart in marked children
      // of `p'.
      for (unsigned np = 0; np < p_size; ++np)
	{
	  // Consider only unmarked children.
	  if (p_seen[np])
	    continue;
	  
	  // Compare with marked children.
	  unsigned np2;
	  const formulae *pnth = p->nth(np);
	  for (np2 = 0; np2 < p_size; ++np2)
	    if (p_seen[np2] && equals(p->nth(np2), pnth))
	      break;
	  
	  // No match?  Too bad.
	  if (np2 == p_size) 
	    return;
	}
      
      // The two formulaes match.
      result_ = true;
    }


    bool 
    equals(const formulae* f1, const formulae* f2)
    {
      equals_visitor v(f1);
      f2->accept(v);
      return v.result();
    }
  }
}