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

* src/ltlvisit/syntimpl.cc: Reduce the number of dynamic_cast<>s.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2010-12-04 17:10:47 +01:00
parent 437af50afe
commit c4a7efb9e0
2 changed files with 15 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

4
ChangeLog
View file

@ -1,3 +1,7 @@
2010-12-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/ltlvisit/syntimpl.cc: Reduce the number of dynamic_cast<>s.
2010-12-04 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2010-12-04 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Preliminary implementation of a tool to generate some interesting Preliminary implementation of a tool to generate some interesting

23
src/ltlvisit/syntimpl.cc
View file

@ -59,7 +59,7 @@ namespace spot
void void
visit(const atomic_prop* ap) visit(const atomic_prop* ap)
{ {
if (dynamic_cast<const atomic_prop*>(f) == ap) if (f == ap)
result_ = true; result_ = true;
} }
@ -220,13 +220,12 @@ namespace spot
} }
bool bool
special_case(const formula* f2) special_case(const binop* f2)
{ {
const binop* fb = dynamic_cast<const binop*>(f); const binop* fb = dynamic_cast<const binop*>(f);
const binop* f2b = dynamic_cast<const binop*>(f2); if (fb && fb->op() == f2->op()
if (fb && f2b && fb->op() == f2b->op() && syntactic_implication(f2->first(), fb->first())
&& syntactic_implication(f2b->first(), fb->first()) && syntactic_implication(f2->second(), fb->second()))
&& syntactic_implication(f2b->second(), fb->second()))
return true; return true;
return false; return false;
} }
@ -284,9 +283,9 @@ namespace spot
case unop::F: case unop::F:
{ {
/* F(a) = true U a */ /* F(a) = true U a */
const formula* tmp = binop::instance(binop::U, const binop* tmp = binop::instance(binop::U,
constant::true_instance(), constant::true_instance(),
f1->clone()); f1->clone());
if (special_case(tmp)) if (special_case(tmp))
{ {
result_ = true; result_ = true;
@ -301,9 +300,9 @@ namespace spot
case unop::G: case unop::G:
{ {
/* G(a) = false R a */ /* G(a) = false R a */
const formula* tmp = binop::instance(binop::R, const binop* tmp = binop::instance(binop::R,
constant::false_instance(), constant::false_instance(),
f1->clone()); f1->clone());
if (special_case(tmp)) if (special_case(tmp))
{ {
result_ = true; result_ = true;