alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/ltlast/formulae.hh (formulae::equals): Remove.

Browse source 
* src/ltlast/unop.hh (unop::equals): Remove.
* src/ltlast/unop.cc (unop::equals): Remove.
* src/ltlast/binop.hh (binop::equals): Remove.
* src/ltlast/binop.cc (binop::equals): Remove.
* src/ltlast/multop.hh (multop::equals): Remove.
* src/ltlast/multop.cc (multop::equals): Remove.
* src/ltlast/atomic_prop.hh (atomic_prop::equals): Remove.
* src/ltlast/atomic_prop.cc (atomic_prop::equals): Remove.
* src/ltlast/constant.hh (constant::equals): Remove.
* src/ltlast/constant.cc (constant::equals): Remove.
This commit is contained in:
Alexandre Duret-Lutz 2003-04-15 11:48:36 +00:00
parent f0a8d0aeb3
commit dfc82ee3f0
12 changed files with 12 additions and 74 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/ltlast/multop.cc
View file

@ -60,38 +60,6 @@ namespace spot
return op_;
}
bool
multop::equals(const formulae* f) const
{
// This check is a bit more complicated than other checks
// because And(a, b, c) is equal to And(c, a, b, a).
const multop* p1 = dynamic_cast<const multop*>(f);
if (!p1 || p1->op() != op())
return false;
const multop* p2 = this;
unsigned s1 = p1->size();
unsigned s2 = p2->size();
if (s1 > s2)
{
std::swap(s1, s2);
std::swap(p1, p2);
}
for (unsigned n1 = 0; n1 < s1; ++n1)
{
unsigned n2;
for (n2 = 0; n2 < s2; ++n2)
{
if (p1->nth(n1)->equals(p2->nth(n2)))
break;
}
if (n2 == s2)
return false;
}
return true;
}
const char*
multop::op_name() const
{