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

Get rid of all dynamic_cast<>s while working on LTL formulae.

Browse source 
They are too slow.

* src/ltlast/formula.hh (opkind, kind, kind_): Use an enum
to indicate the actual kind of the formula.  This way we can
check the kind of a formula without relying on dynamic_cast.
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc,
src/ltlast/multop.cc, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc: Adjust constructors.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/mark.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc: Replace all dynamic_cast by a
call to kind() followed by a static_cast.
This commit is contained in:
Alexandre Duret-Lutz 2010-12-09 13:19:44 +01:00
parent 48cde88b9b
commit 957ba664b7
15 changed files with 743 additions and 609 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ltlast/atomic_prop.cc
View file

@ -32,7 +32,7 @@ namespace spot
{
atomic_prop::atomic_prop(const std::string& name, environment& env)
: name_(name), env_(&env)
: ref_formula(AtomicProp), name_(name), env_(&env)
{
is.boolean = true;
is.sugar_free_boolean = true;

2
src/ltlast/automatop.cc
View file

@ -28,7 +28,7 @@ namespace spot
namespace ltl
{
automatop::automatop(const nfa::ptr nfa, vec* v, bool negated)
: nfa_(nfa), children_(v), negated_(negated)
: ref_formula(AutomatOp), nfa_(nfa), children_(v), negated_(negated)
{
is.boolean = false;
is.sugar_free_boolean = true;

2
src/ltlast/binop.cc
View file

@ -34,7 +34,7 @@ namespace spot
namespace ltl
{
binop::binop(type op, formula* first, formula* second)
: op_(op), first_(first), second_(second)
: ref_formula(BinOp), op_(op), first_(first), second_(second)
{
// Beware: (f U g) is purely eventual if both operands
// are purely eventual, unlike in the proceedings of

6
src/ltlast/bunop.cc
View file

@ -31,7 +31,7 @@ namespace spot
namespace ltl
{
bunop::bunop(type op, formula* child, unsigned min, unsigned max)
: op_(op), child_(child), min_(min), max_(max)
: ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max)
{
props = child->get_props();
@ -314,9 +314,9 @@ namespace spot
// - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)]
// if i*(min+1)<=j(min)+1.
bunop* s = dynamic_cast<bunop*>(child);
if (s)
if (child->kind() == BUnOp)
{
bunop* s = static_cast<bunop*>(child);
unsigned i = s->min();
unsigned j = s->max();

2
src/ltlast/constant.cc
View file

@ -34,7 +34,7 @@ namespace spot
constant constant::empty_word_instance_(constant::EmptyWord);
constant::constant(type val)
: val_(val)
: formula(Constant), val_(val)
{
switch (val)
{

20
src/ltlast/formula.hh
View file

@ -71,11 +71,20 @@ namespace spot
class formula
{
public:
formula() : count_(max_count++)
/// Kind of a sub-formula
enum opkind { Constant,
AtomicProp,
UnOp,
BinOp,
MultOp,
BUnOp,
AutomatOp };
formula(opkind k) : count_(max_count++), kind_(k)
{
// If the counter of formulae ever loops, we want to skip the
// first three values, because they are permanently associated
// to constants, and its convenient to have constants smaller
// to constants, and it is convenient to have constants smaller
// than all other formulae.
if (max_count == 0)
max_count = 3;
@ -100,6 +109,12 @@ namespace spot
/// Return a canonic representation of the formula
virtual std::string dump() const = 0;
/// Return the kind of the top-level operator.
opkind kind() const
{
return kind_;
}
////////////////
// Properties //
////////////////
@ -279,6 +294,7 @@ namespace spot
private:
/// \brief Number of formulae created so far.
static size_t max_count;
opkind kind_;
};
/// \brief Strict Weak Ordering for <code>const formula*</code>.

39
src/ltlast/multop.cc
View file

@ -34,7 +34,7 @@ namespace spot
namespace ltl
{
multop::multop(type op, vec* v)
: op_(op), children_(v)
: ref_formula(MultOp), op_(op), children_(v)
{
unsigned s = v->size();
assert(s > 1);
@ -177,26 +177,27 @@ namespace spot
vec::iterator i = v->begin();
while (i != v->end())
{
multop* p = dynamic_cast<multop*>(*i);
if (p && p->op() == op)
if ((*i)->kind() == MultOp)
{
unsigned ps = p->size();
for (unsigned n = 0; n < ps; ++n)
inlined.push_back(p->nth(n)->clone());
(*i)->destroy();
i = v->erase(i);
}
else
{
// All operator except "Concat" and "Fusion" are
// commutative, so we just keep a list of the inlined
// arguments that should later be added to the vector.
// For concat we have to keep track of the order of
// all the arguments.
if (op == Concat || op == Fusion)
inlined.push_back(*i);
++i;
multop* p = static_cast<multop*>(*i);
if (p->op() == op)
{
unsigned ps = p->size();
for (unsigned n = 0; n < ps; ++n)
inlined.push_back(p->nth(n)->clone());
(*i)->destroy();
i = v->erase(i);
continue;
}
}
// All operator except "Concat" and "Fusion" are
// commutative, so we just keep a list of the inlined
// arguments that should later be added to the vector.
// For concat we have to keep track of the order of
// all the arguments.
if (op == Concat || op == Fusion)
inlined.push_back(*i);
++i;
}
if (op == Concat || op == Fusion)
*v = inlined;

6
src/ltlast/refformula.cc
View file

@ -1,3 +1,5 @@
// Copyright (C) 2010 Laboratoire de Recherche de Developpement de
// l'EPITA (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
@ -26,8 +28,8 @@ namespace spot
{
namespace ltl
{
ref_formula::ref_formula()
: ref_counter_(0)
ref_formula::ref_formula(opkind k)
: formula(k), ref_counter_(0)
{
}

10
src/ltlast/refformula.hh
View file

@ -1,6 +1,8 @@
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
// Copyright (C) 2010 Laboratoire de Recherche de Developpement de
// l'EPITA (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
@ -37,7 +39,7 @@ namespace spot
{
protected:
virtual ~ref_formula();
ref_formula();
ref_formula(opkind k);
void ref_();
bool unref_();
/// Number of references to this formula.

19
src/ltlast/unop.cc
View file

@ -33,13 +33,13 @@ namespace spot
namespace ltl
{
unop::unop(type op, formula* child)
: op_(op), child_(child)
: ref_formula(UnOp), op_(op), child_(child)
{
props = child->get_props();
switch (op)
{
case Not:
is.in_nenoform = !!dynamic_cast<atomic_prop*>(child);
is.in_nenoform = (child->kind() == AtomicProp);
is.accepting_eword = false;
break;
case X:
@ -163,10 +163,13 @@ namespace spot
case F:
case G:
{
// F and G are idempotent.
unop* u = dynamic_cast<unop*>(child);
if (u && u->op() == op)
return u;
if (child->kind() == UnOp)
{
// F and G are idempotent.
unop* u = static_cast<unop*>(child);
if (u->op() == op)
return u;
}
// F(0) = G(0) = 0
// F(1) = G(1) = 1
@ -191,9 +194,9 @@ namespace spot
return bunop::instance(bunop::Star,
constant::true_instance(), 1);
unop* u = dynamic_cast<unop*>(child);
if (u)
if (child->kind() == UnOp)
{
unop* u = static_cast<unop*>(child);
// "Not" is an involution.
if (u->op() == op)
{

910
src/ltlvisit/basicreduce.cc
View file

File diff suppressed because it is too large Load diff

4
src/ltlvisit/mark.cc
View file

@ -221,13 +221,13 @@ namespace spot
{
formula* f = mo->nth(i);
binop* bo = dynamic_cast<binop*>(f);
if (!bo)
if (f->kind() != formula::BinOp)
{
res->push_back(recurse(f));
}
else
{
binop* bo = static_cast<binop*>(f);
switch (bo->op())
{
case binop::Xor:

136
src/ltlvisit/reduce.cc
View file

@ -179,16 +179,17 @@ namespace spot
}
/* a < b => a U (b U c) = (b U c) */
/* a < b => a U (b W c) = (b W c) */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && (bo->op() == binop::U || bo->op() == binop::W)
&& syntactic_implication(f1, bo->first()))
{
result_ = f2;
f1->destroy();
return;
}
}
if (f2->kind() == formula::BinOp)
{
binop* bo = static_cast<binop*>(f2);
if ((bo->op() == binop::U || bo->op() == binop::W)
&& syntactic_implication(f1, bo->first()))
{
result_ = f2;
f1->destroy();
return;
}
}
break;
case binop::R:
@ -206,30 +207,29 @@ namespace spot
f1->destroy();
return;
}
/* b < a => a R (b R c) = b R c */
/* b < a => a R (b M c) = b M c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && (bo->op() == binop::R || bo->op() == binop::M)
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
f1->destroy();
return;
}
}
/* a < b => a R (b R c) = a R c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::R
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::R, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
if (f2->kind() == formula::BinOp)
{
/* b < a => a R (b R c) = b R c */
/* b < a => a R (b M c) = b M c */
binop* bo = static_cast<binop*>(f2);
if ((bo->op() == binop::R || bo->op() == binop::M)
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
f1->destroy();
return;
}
/* a < b => a R (b R c) = a R c */
if (bo->op() == binop::R
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::R, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
break;
case binop::W:
@ -249,16 +249,17 @@ namespace spot
return;
}
/* a < b => a W (b W c) = (b W c) */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::W
&& syntactic_implication(f1, bo->first()))
{
result_ = f2;
f1->destroy();
return;
}
}
if (f2->kind() == formula::BinOp)
{
binop* bo = static_cast<binop*>(f2);
if (bo->op() == binop::W
&& syntactic_implication(f1, bo->first()))
{
result_ = f2;
f1->destroy();
return;
}
}
break;
case binop::M:
@ -277,30 +278,29 @@ namespace spot
f2->destroy();
return;
}
/* b < a => a M (b M c) = b M c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && bo->op() == binop::M
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
f1->destroy();
return;
}
}
/* a < b => a M (b M c) = a M c */
/* a < b => a M (b R c) = a M c */
{
binop* bo = dynamic_cast<binop*>(f2);
if (bo && (bo->op() == binop::M || bo->op() == binop::R)
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::M, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
if (f2->kind() == formula::BinOp)
{
/* b < a => a M (b M c) = b M c */
binop* bo = static_cast<binop*>(f2);
if (bo->op() == binop::M
&& syntactic_implication(bo->first(), f1))
{
result_ = f2;
f1->destroy();
return;
}
/* a < b => a M (b M c) = a M c */
/* a < b => a M (b R c) = a M c */
if ((bo->op() == binop::M || bo->op() == binop::R)
&& syntactic_implication(f1, bo->first()))
{
result_ = binop::instance(binop::M, f1,
bo->second()->clone());
f2->destroy();
return;
}
}
break;
}
}

188
src/ltlvisit/syntimpl.cc
View file

@ -96,8 +96,10 @@ namespace spot
return;
case unop::X:
{
const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::X)
if (f->kind() != formula::UnOp)
return;
const unop* op = static_cast<const unop*>(f);
if (op->op() == unop::X)
result_ = syntactic_implication(op->child(), f1);
}
return;
@ -124,8 +126,6 @@ namespace spot
{
const formula* f1 = bo->first();
const formula* f2 = bo->second();
const binop* fb = dynamic_cast<const binop*>(f);
const unop* fu = dynamic_cast<const unop*>(f);
switch (bo->op())
{
case binop::Xor:
@ -141,39 +141,55 @@ namespace spot
result_ = true;
return;
case binop::R:
if (fb && fb->op() == binop::R)
if (syntactic_implication(fb->first(), f1) &&
syntactic_implication(fb->second(), f2))
{
result_ = true;
return;
}
if (fu && fu->op() == unop::G)
if (f1 == constant::false_instance() &&
syntactic_implication(fu->child(), f2))
{
result_ = true;
return;
}
if (f->kind() == formula::BinOp)
{
const binop* fb = static_cast<const binop*>(f);
if (fb->op() == binop::R
&& syntactic_implication(fb->first(), f1)
&& syntactic_implication(fb->second(), f2))
{
result_ = true;
return;
}
}
if (f->kind() == formula::UnOp)
{
const unop* fu = static_cast<const unop*>(f);
if (fu->op() == unop::G
&& f1 == constant::false_instance()
&& syntactic_implication(fu->child(), f2))
{
result_ = true;
return;
}
}
if (syntactic_implication(f, f1)
&& syntactic_implication(f, f2))
result_ = true;
return;
case binop::M:
if (fb && fb->op() == binop::M)
if (syntactic_implication(fb->first(), f1) &&
syntactic_implication(fb->second(), f2))
{
result_ = true;
return;
}
if (fu && fu->op() == unop::F)
if (f2 == constant::true_instance() &&
syntactic_implication(fu->child(), f1))
if (f->kind() == formula::BinOp)
{
const binop* fb = static_cast<const binop*>(f);
if (fb->op() == binop::M
&& syntactic_implication(fb->first(), f1)
&& syntactic_implication(fb->second(), f2))
{
result_ = true;
return;
}
}
if (f->kind() == formula::UnOp)
{
const unop* fu = static_cast<const unop*>(f);
if (fu->op() == unop::F
&& f2 == constant::true_instance()
&& syntactic_implication(fu->child(), f1))
{
result_ = true;
return;
}
}
if (syntactic_implication(f, f1)
&& syntactic_implication(f, f2))
result_ = true;
@ -238,8 +254,10 @@ namespace spot
bool
special_case(const binop* f2)
{
const binop* fb = dynamic_cast<const binop*>(f);
if (fb && fb->op() == f2->op()
if (f->kind() != formula::BinOp)
return false;
const binop* fb = static_cast<const binop*>(f);
if (fb->op() == f2->op()
&& syntactic_implication(f2->first(), fb->first())
&& syntactic_implication(f2->second(), fb->second()))
return true;
@ -249,10 +267,9 @@ namespace spot
bool
special_case_check(const formula* f2)
{
const binop* f2b = dynamic_cast<const binop*>(f2);
if (!f2b)
if (f2->kind() != formula::BinOp)
return false;
return special_case(f2b);
return special_case(static_cast<const binop*>(f2));
}
int
@ -307,11 +324,12 @@ namespace spot
result_ = true;
return;
case unop::X:
{
const unop* op = dynamic_cast<const unop*>(f);
if (op && op->op() == unop::X)
result_ = syntactic_implication(f1, op->child());
}
if (f->kind() == formula::UnOp)
{
const unop* op = static_cast<const unop*>(f);
if (op->op() == unop::X)
result_ = syntactic_implication(f1, op->child());
}
return;
case unop::F:
{
@ -367,8 +385,6 @@ namespace spot
const formula* f1 = bo->first();
const formula* f2 = bo->second();
const binop* fb = dynamic_cast<const binop*>(f);
const unop* fu = dynamic_cast<const unop*>(f);
switch (bo->op())
{
case binop::Xor:
@ -380,63 +396,87 @@ namespace spot
return;
case binop::U:
/* (a < c) && (c < d) => a U b < c U d */
if (fb && fb->op() == binop::U)
if (syntactic_implication(f1, fb->first()) &&
syntactic_implication(f2, fb->second()))
{
result_ = true;
return;
}
if (fu && fu->op() == unop::F)
if (f1 == constant::true_instance() &&
syntactic_implication(f2, fu->child()))
{
result_ = true;
return;
}
if (f->kind() == formula::BinOp)
{
const binop* fb = static_cast<const binop*>(f);
if (fb->op() == binop::U
&& syntactic_implication(f1, fb->first())
&& syntactic_implication(f2, fb->second()))
{
result_ = true;
return;
}
}
if (f->kind() == formula::UnOp)
{
const unop* fu = static_cast<const unop*>(f);
if (fu->op() == unop::F
&& f1 == constant::true_instance()
&& syntactic_implication(f2, fu->child()))
{
result_ = true;
return;
}
}
if (syntactic_implication(f1, f)
&& syntactic_implication(f2, f))
result_ = true;
return;
case binop::W:
/* (a < c) && (c < d) => a W b < c W d */
if (fb && fb->op() == binop::W)
if (syntactic_implication(f1, fb->first()) &&
syntactic_implication(f2, fb->second()))
{
result_ = true;
return;
}
if (fu && fu->op() == unop::G)
if (f2 == constant::false_instance() &&
syntactic_implication(f1, fu->child()))
{
result_ = true;
return;
}
if (f->kind() == formula::BinOp)
{
const binop* fb = static_cast<const binop*>(f);
if (fb->op() == binop::W
&& syntactic_implication(f1, fb->first())
&& syntactic_implication(f2, fb->second()))
{
result_ = true;
return;
}
}
if (f->kind() == formula::UnOp)
{
const unop* fu = static_cast<const unop*>(f);
if (fu && fu->op() == unop::G
&& f2 == constant::false_instance()
&& syntactic_implication(f1, fu->child()))
{
result_ = true;
return;
}
}
if (syntactic_implication(f1, f)
&& syntactic_implication(f2, f))
result_ = true;
return;
case binop::R:
if (fu && fu->op() == unop::G)
if (f1 == constant::false_instance() &&
syntactic_implication(f2, fu->child()))
if (f->kind() == formula::UnOp)
{
const unop* fu = static_cast<const unop*>(f);
if (fu->op() == unop::G
&& f1 == constant::false_instance()
&& syntactic_implication(f2, fu->child()))
{
result_ = true;
return;
}
}
if (syntactic_implication(f2, f))
result_ = true;
return;
case binop::M:
if (fu && fu->op() == unop::F)
if (f2 == constant::true_instance() &&
syntactic_implication(f1, fu->child()))
if (f->kind() == formula::UnOp)
{
const unop* fu = static_cast<const unop*>(f);
if (fu->op() == unop::F
&& f2 == constant::true_instance()
&& syntactic_implication(f1, fu->child()))
{
result_ = true;
return;
}
}
if (syntactic_implication(f2, f))
result_ = true;
return;

6
src/ltlvisit/tostring.cc
View file

@ -188,7 +188,7 @@ namespace spot
// a[*] is OK, no need to print {a}[*].
// However want braces for {!a}[*], the only unary
// operator that can be nested with [*].
bool need_parent = !!dynamic_cast<const unop*>(bo->child());
bool need_parent = (bo->child()->kind() == formula::UnOp);
if (need_parent || full_parent_)
openp();
@ -206,7 +206,7 @@ namespace spot
top_level_ = false;
// The parser treats F0, F1, G0, G1, X0, and X1 as atomic
// propositions. So make sure we output F(0), G(1), etc.
bool need_parent = !!dynamic_cast<const constant*>(uo->child());
bool need_parent = (uo->child()->kind() == formula::Constant);
bool top_level = top_level_;
if (full_parent_)
@ -456,7 +456,7 @@ namespace spot
case unop::X:
// The parser treats X0, and X1 as atomic
// propositions. So make sure we output X(0) and X(1).
need_parent = !!dynamic_cast<const constant*>(uo->child());
need_parent = (uo->child()->kind() == formula::Constant);
if (full_parent_)
need_parent = false;
os_ << "X";