From 957ba664b7553e6de383584350145a170e620366 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 9 Dec 2010 13:19:44 +0100 Subject: [PATCH] Get rid of all dynamic_cast<>s while working on LTL formulae. 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. --- src/ltlast/atomic_prop.cc | 2 +- src/ltlast/automatop.cc | 2 +- src/ltlast/binop.cc | 2 +- src/ltlast/bunop.cc | 6 +- src/ltlast/constant.cc | 2 +- src/ltlast/formula.hh | 20 +- src/ltlast/multop.cc | 39 +- src/ltlast/refformula.cc | 6 +- src/ltlast/refformula.hh | 10 +- src/ltlast/unop.cc | 19 +- src/ltlvisit/basicreduce.cc | 910 +++++++++++++++++++----------------- src/ltlvisit/mark.cc | 4 +- src/ltlvisit/reduce.cc | 136 +++--- src/ltlvisit/syntimpl.cc | 188 +++++--- src/ltlvisit/tostring.cc | 6 +- 15 files changed, 743 insertions(+), 609 deletions(-) diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 1f7c17a89..e1727a124 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -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; diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc index 69c674a84..ab13be12a 100644 --- a/src/ltlast/automatop.cc +++ b/src/ltlast/automatop.cc @@ -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; diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index cf0363525..c3b1bba99 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -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 diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index c9bb31af7..3f3d46de1 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -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(child); - if (s) + if (child->kind() == BUnOp) { + bunop* s = static_cast(child); unsigned i = s->min(); unsigned j = s->max(); diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 2fb9dc834..2fc89c19f 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -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) { diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index 5a323f030..e19aed201 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -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 const formula*. diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index dc5c32ab5..df1425507 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -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(*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(*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; diff --git a/src/ltlast/refformula.cc b/src/ltlast/refformula.cc index 06ad2dad7..d6b3ef7c1 100644 --- a/src/ltlast/refformula.cc +++ b/src/ltlast/refformula.cc @@ -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) { } diff --git a/src/ltlast/refformula.hh b/src/ltlast/refformula.hh index b086fdd84..2a1566bfe 100644 --- a/src/ltlast/refformula.hh +++ b/src/ltlast/refformula.hh @@ -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. diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index b7129e6b8..e65a43b28 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -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(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(child); - if (u && u->op() == op) - return u; + if (child->kind() == UnOp) + { + // F and G are idempotent. + unop* u = static_cast(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(child); - if (u) + if (child->kind() == UnOp) { + unop* u = static_cast(child); // "Not" is an involution. if (u->op() == op) { diff --git a/src/ltlvisit/basicreduce.cc b/src/ltlvisit/basicreduce.cc index 190b915b7..ae5f89712 100644 --- a/src/ltlvisit/basicreduce.cc +++ b/src/ltlvisit/basicreduce.cc @@ -33,27 +33,31 @@ namespace spot bool is_GF(const formula* f) { - const unop* op = dynamic_cast(f); - if (op && op->op() == unop::G) - { - const unop* opchild = dynamic_cast(op->child()); - if (opchild && opchild->op() == unop::F) - return true; - } - return false; + if (f->kind() != formula::UnOp) + return false; + const unop* op = static_cast(f); + if (op->op() != unop::G) + return false; + const formula* c = op->child(); + if (c->kind() != formula::UnOp) + return false; + const unop* opchild = static_cast(c); + return opchild->op() == unop::F; } bool is_FG(const formula* f) { - const unop* op = dynamic_cast(f); - if (op && op->op() == unop::F) - { - const unop* opchild = dynamic_cast(op->child()); - if (opchild && opchild->op() == unop::G) - return true; - } - return false; + if (f->kind() != formula::UnOp) + return false; + const unop* op = static_cast(f); + if (op->op() != unop::F) + return false; + const formula* c = op->child(); + if (c->kind() != formula::UnOp) + return false; + const unop* opchild = static_cast(c); + return opchild->op() == unop::G; } namespace @@ -134,7 +138,7 @@ namespace spot case unop::X: // X(true) = true // X(false) = false - if (dynamic_cast(result_)) + if (result_->kind() == formula::Constant) return; // XGF(f) = GF(f) @@ -143,9 +147,9 @@ namespace spot // X(f1 & GF(f2)) = X(f1) & GF(F2) // X(f1 | GF(f2)) = X(f1) | GF(F2) - mo = dynamic_cast(result_); - if (mo) + if (result_->kind() == formula::MultOp) { + mo = static_cast(result_); result_ = param_case(mo, unop::X, mo->op()); return; } @@ -156,22 +160,24 @@ namespace spot case unop::F: // F(true) = true // F(false) = false - if (dynamic_cast(result_)) + if (result_->kind() == formula::Constant) return; // FX(a) = XF(a) - u = dynamic_cast(result_); - if (u && u->op() == unop::X) + if (result_->kind() == formula::UnOp) { - formula* res = - unop::instance(unop::X, - unop::instance(unop::F, - basic_reduce(u->child()))); - u->destroy(); - // FXX(a) = XXF(a) ... - result_ = basic_reduce(res); - res->destroy(); - return; + u = static_cast(result_); + if (u->op() == unop::X) + { + formula* res = + unop::instance(unop::X, unop::instance + (unop::F, basic_reduce(u->child()))); + u->destroy(); + // FXX(a) = XXF(a) ... + result_ = basic_reduce(res); + res->destroy(); + return; + } } #if 0 @@ -189,11 +195,14 @@ namespace spot // GF(f2)) | (a & GF(b))) is indeed easier to translate. // // So let's not consider this rewriting rule. - mo = dynamic_cast(result_); - if (mo && mo->op() == multop::And) + if (result_->kind() == formula::MultOp) { - result_ = param_case(mo, unop::F, multop::And); - return; + mo = static_cast(result_); + if (mo->op() == multop::And) + { + result_ = param_case(mo, unop::F, multop::And); + return; + } } #endif @@ -203,41 +212,49 @@ namespace spot case unop::G: // G(true) = true // G(false) = false - if (dynamic_cast(result_)) + if (result_->kind() == formula::Constant) return; // G(a R b) = G(b) - bo = dynamic_cast(result_); - if (bo && bo->op() == binop::R) + if (result_->kind() == formula::BinOp) { - result_ = unop::instance(unop::G, - basic_reduce(bo->second())); - bo->destroy(); - return; + bo = static_cast(result_); + if (bo->op() == binop::R) + { + result_ = unop::instance(unop::G, + basic_reduce(bo->second())); + bo->destroy(); + return; + } } // GX(a) = XG(a) - u = dynamic_cast(result_); - if (u && u->op() == unop::X) + if (result_->kind() == formula::UnOp) { - formula* res = - unop::instance(unop::X, - unop::instance(unop::G, - basic_reduce(u->child()))); - u->destroy(); - // GXX(a) = XXG(a) ... - // GXF(a) = XGF(a) = GF(a) ... - result_ = basic_reduce(res); - res->destroy(); - return; + u = static_cast(result_); + if (u->op() == unop::X) + { + formula* res = + unop::instance(unop::X, unop::instance + (unop::G, basic_reduce(u->child()))); + u->destroy(); + // GXX(a) = XXG(a) ... + // GXF(a) = XGF(a) = GF(a) ... + result_ = basic_reduce(res); + res->destroy(); + return; + } } // G(f1 | GF(f2)) = G(f1) | GF(F2) - mo = dynamic_cast(result_); - if (mo && mo->op() == multop::Or) + if (result_->kind() == formula::MultOp) { - result_ = param_case(mo, unop::G, multop::Or); - return; + mo = static_cast(result_); + if (mo->op() == multop::Or) + { + result_ = param_case(mo, unop::G, multop::Or); + return; + } } result_ = unop::instance(unop::G, result_); @@ -297,19 +314,23 @@ namespace spot // a R true = true // a W true = true // a M false = false - if (dynamic_cast(f2)) + if (f2->kind() == formula::Constant) { result_ = f2; f1->destroy(); return; } + // Same effect as dynamic_cast, only faster. + unop* fu1 = + (f1->kind() == formula::UnOp) ? static_cast(f1) : 0; + unop* fu2 = + (f2->kind() == formula::UnOp) ? static_cast(f2) : 0; + // X(a) U X(b) = X(a U b) // X(a) R X(b) = X(a R b) // X(a) W X(b) = X(a W b) // X(a) M X(b) = X(a M b) - unop* fu1 = dynamic_cast(f1); - unop* fu2 = dynamic_cast(f2); if (fu1 && fu2 && fu1->op() == unop::X && fu2->op() == unop::X) @@ -337,29 +358,33 @@ namespace spot // a U (b | G(a)) = a W b // a W (b | G(a)) = a W b - multop* fm2 = dynamic_cast(f2); - if (fm2 && fm2->op() == multop::Or) + if (f2->kind() == formula::MultOp) { - int s = fm2->size(); - for (int i = 0; i < s; ++i) + multop* fm2 = static_cast(f2); + if (fm2->op() == multop::Or) { - unop* c = dynamic_cast(fm2->nth(i)); - if (c && c->op() == unop::G && c->child() == f1) + int s = fm2->size(); + for (int i = 0; i < s; ++i) { - multop::vec* v = new multop::vec; - v->reserve(s - 1); - int j; - for (j = 0; j < i; ++j) - v->push_back(fm2->nth(j)->clone()); - // skip j=i - for (++j; j < s; ++j) - v->push_back(fm2->nth(j)->clone()); - result_ = - binop::instance(binop::W, f1, - multop::instance(multop::Or, - v)); - f2->destroy(); - return; + if (fm2->nth(i)->kind() != formula::UnOp) + continue; + unop* c = static_cast(fm2->nth(i)); + if (c->op() == unop::G && c->child() == f1) + { + multop::vec* v = new multop::vec; + v->reserve(s - 1); + int j; + for (j = 0; j < i; ++j) + v->push_back(fm2->nth(j)->clone()); + // skip j=i + for (++j; j < s; ++j) + v->push_back(fm2->nth(j)->clone()); + result_ = binop::instance + (binop::W, f1, + multop::instance(multop::Or, v)); + f2->destroy(); + return; + } } } } @@ -377,29 +402,33 @@ namespace spot // a R (b & F(a)) = a M b // a M (b & F(a)) = a M b - multop* fm2 = dynamic_cast(f2); - if (fm2 && fm2->op() == multop::And) + if (f2->kind() == formula::MultOp) { - int s = fm2->size(); - for (int i = 0; i < s; ++i) + multop* fm2 = static_cast(f2); + if (fm2->op() == multop::And) { - unop* c = dynamic_cast(fm2->nth(i)); - if (c && c->op() == unop::F && c->child() == f1) + int s = fm2->size(); + for (int i = 0; i < s; ++i) { - multop::vec* v = new multop::vec; - v->reserve(s - 1); - int j; - for (j = 0; j < i; ++j) - v->push_back(fm2->nth(j)->clone()); - // skip j=i - for (++j; j < s; ++j) - v->push_back(fm2->nth(j)->clone()); - result_ = - binop::instance(binop::M, f1, - multop::instance(multop::And, - v)); - f2->destroy(); - return; + if (fm2->nth(i)->kind() != formula::UnOp) + continue; + unop* c = static_cast(fm2->nth(i)); + if (c->op() == unop::F && c->child() == f1) + { + multop::vec* v = new multop::vec; + v->reserve(s - 1); + int j; + for (j = 0; j < i; ++j) + v->push_back(fm2->nth(j)->clone()); + // skip j=i + for (++j; j < s; ++j) + v->push_back(fm2->nth(j)->clone()); + result_ = binop::instance + (binop::M, f1, + multop::instance(multop::And, v)); + f2->destroy(); + return; + } } } } @@ -449,175 +478,196 @@ namespace spot // of the vector to mark them as redundant. Skip them. if (!*i) continue; - unop* uo = dynamic_cast(*i); - binop* bo = dynamic_cast(*i); - if (uo) - { - if (uo->op() == unop::X) - { - // Xa & Xb = X(a & b) - tmpX->push_back(uo->child()->clone()); - } - else if (is_FG(*i)) - { - // FG(a) & FG(b) = FG(a & b) - unop* uo2 = dynamic_cast(uo->child()); - tmpFG->push_back(uo2->child()->clone()); - } - else if (uo->op() == unop::G) - { - // G(a) & G(b) = G(a & b) - tmpG->push_back(uo->child()->clone()); - } - else if (uo->op() == unop::F) - { - // F(a) & (a R b) = a M b - // F(a) & (a M b) = a M b - // F(a) & (b W a) = b U a - // F(a) & (b U a) = b U a - formula* a = uo->child(); - bool rewritten = false; - for (multop::vec::iterator j = i; - j != res->end(); ++j) - { - if (!*j) - continue; - binop* b = dynamic_cast(*j); - if (b && (b->op() == binop::R - || b->op() == binop::M) - && b->first() == a) - { - formula* r = - binop::instance(binop::M, - a->clone(), - b->second()->clone()); - tmpOther->push_back(r); - (*j)->destroy(); - *j = 0; - rewritten = true; - } - else if (b && (b->op() == binop::W - || b->op() == binop::U) - && b->second() == a) - { - formula* r = - binop::instance(binop::U, - b->first()->clone(), - a->clone()); - tmpOther->push_back(r); - (*j)->destroy(); - *j = 0; - rewritten = true; - } - } - if (!rewritten) - tmpOther->push_back(uo->clone()); - } - else - { - tmpOther->push_back((*i)->clone()); - } - } - else if (bo) - { - if (bo->op() == binop::U || bo->op() == binop::W) - { - // (a U b) & (c U b) = (a & c) U b - // (a U b) & (c W b) = (a & c) U b - // (a W b) & (c W b) = (a & c) W b - bool weak = true; - formula* ftmp = dynamic_cast(*i)->second(); - multop::vec* right = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); - j++) - { - if (!*j) - continue; - // (a U b) & Fb = a U b. - // (a W b) & Fb = a U b. - unop* uo2 = dynamic_cast(*j); - if (uo2 && uo2->op() == unop::F - && uo2->child() == ftmp) - { - (*j)->destroy(); - *j = 0; - weak = false; - } - binop* bo2 = dynamic_cast(*j); - if (bo2 && (bo2->op() == binop::U - || bo2->op() == binop::W) - && ftmp == bo2->second()) - { - if (bo2->op() == binop::U) - weak = false; - right->push_back(bo2->first()->clone()); - if (j != i) - { - (*j)->destroy(); - *j = 0; - } - } - } - tmpU - ->push_back(binop::instance(weak ? - binop::W : binop::U, - multop:: - instance(multop:: - And, right), - ftmp->clone())); - } - else if (bo->op() == binop::R || bo->op() == binop::M) - { - // (a R b) & (a R c) = a R (b & c) - // (a R b) & (a M c) = a M (b & c) - bool weak = true; - formula* ftmp = dynamic_cast(*i)->first(); - multop::vec* right = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); - j++) - { - if (!*j) - continue; - // (a R b) & Fa = a M b. - // (a M b) & Fa = a M b. - unop* uo2 = dynamic_cast(*j); - if (uo2 && uo2->op() == unop::F - && uo2->child() == ftmp) - { - (*j)->destroy(); - *j = 0; - weak = false; - } - binop* bo2 = dynamic_cast(*j); - if (bo2 && (bo2->op() == binop::R - || bo2->op() == binop::M) - && ftmp == bo2->first()) - { - if (bo2->op() == binop::M) - weak = false; - right->push_back(bo2->second()->clone()); - if (j != i) - { - (*j)->destroy(); - *j = 0; - } - } - } - tmpR - ->push_back(binop::instance(weak ? - binop::R : binop::M, - ftmp->clone(), - multop:: - instance(multop::And, - right))); - } - else - { - tmpOther->push_back((*i)->clone()); - } - } - else + switch ((*i)->kind()) { + case formula::UnOp: + { + unop* uo = static_cast(*i); + if (uo->op() == unop::X) + { + // Xa & Xb = X(a & b) + tmpX->push_back(uo->child()->clone()); + } + else if (is_FG(*i)) + { + // FG(a) & FG(b) = FG(a & b) + unop* uo2 = static_cast(uo->child()); + tmpFG->push_back(uo2->child()->clone()); + } + else if (uo->op() == unop::G) + { + // G(a) & G(b) = G(a & b) + tmpG->push_back(uo->child()->clone()); + } + else if (uo->op() == unop::F) + { + // F(a) & (a R b) = a M b + // F(a) & (a M b) = a M b + // F(a) & (b W a) = b U a + // F(a) & (b U a) = b U a + formula* a = uo->child(); + bool rewritten = false; + for (multop::vec::iterator j = i; + j != res->end(); ++j) + { + if (!*j) + continue; + if ((*i)->kind() != formula::BinOp) + continue; + binop* b = static_cast(*j); + if ((b->op() == binop::R || b->op() == binop::M) + && b->first() == a) + { + formula* r = + binop::instance(binop::M, + a->clone(), + b->second()->clone()); + tmpOther->push_back(r); + (*j)->destroy(); + *j = 0; + rewritten = true; + } + else if ((b->op() == binop::W + || b->op() == binop::U) + && b->second() == a) + { + formula* r = + binop::instance(binop::U, + b->first()->clone(), + a->clone()); + tmpOther->push_back(r); + (*j)->destroy(); + *j = 0; + rewritten = true; + } + } + if (!rewritten) + tmpOther->push_back(uo->clone()); + } + else + { + tmpOther->push_back((*i)->clone()); + } + break; + } + case formula::BinOp: + { + binop* bo = static_cast(*i); + if (bo->op() == binop::U || bo->op() == binop::W) + { + // (a U b) & (c U b) = (a & c) U b + // (a U b) & (c W b) = (a & c) U b + // (a W b) & (c W b) = (a & c) W b + bool weak = true; + formula* ftmp = bo->second(); + multop::vec* right = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + // (a U b) & Fb = a U b. + // (a W b) & Fb = a U b. + if ((*j)->kind() == formula::UnOp) + { + unop* uo2 = static_cast(*j); + if (uo2->op() == unop::F + && uo2->child() == ftmp) + { + (*j)->destroy(); + *j = 0; + weak = false; + continue; + } + } + if ((*j)->kind() == formula::BinOp) + { + binop* bo2 = static_cast(*j); + if ((bo2->op() == binop::U + || bo2->op() == binop::W) + && ftmp == bo2->second()) + { + if (bo2->op() == binop::U) + weak = false; + right->push_back(bo2->first()->clone()); + if (j != i) + { + (*j)->destroy(); + *j = 0; + continue; + } + } + } + } + tmpU + ->push_back(binop::instance(weak ? + binop::W : binop::U, + multop:: + instance(multop:: + And, right), + ftmp->clone())); + } + else if (bo->op() == binop::R || bo->op() == binop::M) + { + // (a R b) & (a R c) = a R (b & c) + // (a R b) & (a M c) = a M (b & c) + bool weak = true; + formula* ftmp = bo->first(); + multop::vec* right = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + // (a R b) & Fa = a M b. + // (a M b) & Fa = a M b. + if ((*j)->kind() == formula::UnOp) + { + unop* uo2 = static_cast(*j); + if (uo2->op() == unop::F + && uo2->child() == ftmp) + { + (*j)->destroy(); + *j = 0; + weak = false; + continue; + } + } + if ((*j)->kind() == formula::BinOp) + { + binop* bo2 = static_cast(*j); + if ((bo2->op() == binop::R + || bo2->op() == binop::M) + && ftmp == bo2->first()) + { + if (bo2->op() == binop::M) + weak = false; + right->push_back + (bo2->second()->clone()); + if (j != i) + { + (*j)->destroy(); + *j = 0; + continue; + } + } + } + } + tmpR + ->push_back(binop::instance(weak ? + binop::R : binop::M, + ftmp->clone(), + multop:: + instance(multop::And, + right))); + } + else + { + tmpOther->push_back((*i)->clone()); + } + break; + } + default: tmpOther->push_back((*i)->clone()); } (*i)->destroy(); @@ -630,164 +680,184 @@ namespace spot { if (!*i) continue; - unop* uo = dynamic_cast(*i); - binop* bo = dynamic_cast(*i); - if (uo) + switch ((*i)->kind()) { - if (uo->op() == unop::X) - { - // Xa | Xb = X(a | b) - tmpX->push_back(uo->child()->clone()); - } - else if (is_GF(*i)) - { - // GF(a) | GF(b) = GF(a | b) - unop* uo2 = dynamic_cast(uo->child()); - tmpGF->push_back(uo2->child()->clone()); - } - else if (uo->op() == unop::F) - { - // F(a) | F(b) = F(a | b) - tmpF->push_back(uo->child()->clone()); - } - else if (uo->op() == unop::G) - { - // G(a) | (a U b) = a W b - // G(a) | (a W b) = a W b - formula* a = uo->child(); - bool rewritten = false; - for (multop::vec::iterator j = i; - j != res->end(); ++j) - { - if (!*j) - continue; - binop* b = dynamic_cast(*j); - if (b && (b->op() == binop::U - || b->op() == binop::W) - && b->first() == a) - { - formula* r = - binop::instance(binop::W, - a->clone(), - b->second()->clone()); - tmpOther->push_back(r); - (*j)->destroy(); - *j = 0; - rewritten = true; - } - } - if (!rewritten) - tmpOther->push_back(uo->clone()); - } - else - { - tmpOther->push_back((*i)->clone()); - } - } - else if (bo) - { - if (bo->op() == binop::U || bo->op() == binop::W) - { - // (a U b) | (a U c) = a U (b | c) - // (a W b) | (a U c) = a W (b | c) - bool weak = false; - formula* ftmp = bo->first(); - multop::vec* right = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); - j++) - { - if (!*j) - continue; - // (a U b) | Ga = a W b. - // (a W b) | Ga = a W b. - unop* uo2 = dynamic_cast(*j); - if (uo2 && uo2->op() == unop::G - && uo2->child() == ftmp) - { - (*j)->destroy(); - *j = 0; - weak = true; - } - binop* bo2 = dynamic_cast(*j); - if (bo2 && (bo2->op() == binop::U || - bo2->op() == binop::W) - && ftmp == bo2->first()) - { - if (bo2->op() == binop::W) - weak = true; - right->push_back(bo2->second()->clone()); - if (j != i) - { - (*j)->destroy(); - *j = 0; - } - } - } - tmpU->push_back(binop::instance(weak ? - binop::W : binop::U, - ftmp->clone(), + case formula::UnOp: + { + unop* uo = static_cast(*i); + if (uo->op() == unop::X) + { + // Xa | Xb = X(a | b) + tmpX->push_back(uo->child()->clone()); + } + else if (is_GF(*i)) + { + // GF(a) | GF(b) = GF(a | b) + unop* uo2 = static_cast(uo->child()); + tmpGF->push_back(uo2->child()->clone()); + } + else if (uo->op() == unop::F) + { + // F(a) | F(b) = F(a | b) + tmpF->push_back(uo->child()->clone()); + } + else if (uo->op() == unop::G) + { + // G(a) | (a U b) = a W b + // G(a) | (a W b) = a W b + formula* a = uo->child(); + bool rewritten = false; + for (multop::vec::iterator j = i; + j != res->end(); ++j) + { + if (!*j) + continue; + if ((*j)->kind() != formula::BinOp) + continue; + binop* b = static_cast(*j); + if ((b->op() == binop::U || b->op() == binop::W) + && b->first() == a) + { + formula* r = + binop::instance(binop::W, + a->clone(), + b->second()->clone()); + tmpOther->push_back(r); + (*j)->destroy(); + *j = 0; + rewritten = true; + } + } + if (!rewritten) + tmpOther->push_back(uo->clone()); + } + else + { + tmpOther->push_back((*i)->clone()); + } + break; + } + case formula::BinOp: + { + binop* bo = static_cast(*i); + if (bo->op() == binop::U || bo->op() == binop::W) + { + // (a U b) | (a U c) = a U (b | c) + // (a W b) | (a U c) = a W (b | c) + bool weak = false; + formula* ftmp = bo->first(); + multop::vec* right = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + // (a U b) | Ga = a W b. + // (a W b) | Ga = a W b. + if ((*j)->kind() == formula::UnOp) + { + unop* uo2 = static_cast(*j); + if (uo2->op() == unop::G + && uo2->child() == ftmp) + { + (*j)->destroy(); + *j = 0; + weak = true; + continue; + } + } + if ((*j)->kind() == formula::BinOp) + { + binop* bo2 = static_cast(*j); + if ((bo2->op() == binop::U || + bo2->op() == binop::W) + && ftmp == bo2->first()) + { + if (bo2->op() == binop::W) + weak = true; + right->push_back + (bo2->second()->clone()); + if (j != i) + { + (*j)->destroy(); + *j = 0; + continue; + } + } + } + } + tmpU->push_back(binop::instance(weak ? + binop::W : binop::U, + ftmp->clone(), + multop:: + instance(multop::Or, + right))); + } + else if (bo->op() == binop::R || bo->op() == binop::M) + { + // (a R b) | (c R b) = (a | c) R b + // (a R b) | (c M b) = (a | c) R b + // (a M b) | (c M b) = (a | c) M b + bool weak = false; + formula* ftmp = bo->second(); + multop::vec* right = new multop::vec; + for (multop::vec::iterator j = i; j != res->end(); + j++) + { + if (!*j) + continue; + // (a R b) | Gb = a R b. + // (a M b) | Gb = a R b. + if ((*j)->kind() == formula::UnOp) + { + unop* uo2 = static_cast(*j); + if (uo2->op() == unop::G + && uo2->child() == ftmp) + { + (*j)->destroy(); + *j = 0; + weak = true; + continue; + } + } + if ((*j)->kind() == formula::BinOp) + { + binop* bo2 = static_cast(*j); + if ((bo2->op() == binop::R + || bo2->op() == binop::M) + && ftmp == bo2->second()) + { + if (bo2->op() == binop::R) + weak = true; + right->push_back(bo2->first()->clone()); + if (j != i) + { + (*j)->destroy(); + *j = 0; + continue; + } + } + } + } + tmpR + ->push_back(binop::instance(weak ? + binop::R : binop::M, multop:: instance(multop::Or, - right))); - } - else if (bo->op() == binop::R || bo->op() == binop::M) - { - // (a R b) | (c R b) = (a | c) R b - // (a R b) | (c M b) = (a | c) R b - // (a M b) | (c M b) = (a | c) M b - bool weak = false; - formula* ftmp = dynamic_cast(*i)->second(); - multop::vec* right = new multop::vec; - for (multop::vec::iterator j = i; j != res->end(); - j++) - { - if (!*j) - continue; - // (a R b) | Gb = a R b. - // (a M b) | Gb = a R b. - unop* uo2 = dynamic_cast(*j); - if (uo2 && uo2->op() == unop::G - && uo2->child() == ftmp) - { - (*j)->destroy(); - *j = 0; - weak = true; - } - binop* bo2 = dynamic_cast(*j); - if (bo2 && (bo2->op() == binop::R - || bo2->op() == binop::M) - && ftmp == bo2->second()) - { - if (bo2->op() == binop::R) - weak = true; - right->push_back(bo2->first()->clone()); - if (j != i) - { - (*j)->destroy(); - *j = 0; - } - } - } - tmpR - ->push_back(binop::instance(weak ? - binop::R : binop::M, - multop:: - instance(multop::Or, - right), - ftmp->clone())); - } - else - { - tmpOther->push_back((*i)->clone()); - } - } - else - { + right), + ftmp->clone())); + } + else + { + tmpOther->push_back((*i)->clone()); + } + break; + } + default: tmpOther->push_back((*i)->clone()); } (*i)->destroy(); } - break; case multop::Concat: case multop::AndNLM: diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 73d003472..8ab52cad9 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -221,13 +221,13 @@ namespace spot { formula* f = mo->nth(i); - binop* bo = dynamic_cast(f); - if (!bo) + if (f->kind() != formula::BinOp) { res->push_back(recurse(f)); } else { + binop* bo = static_cast(f); switch (bo->op()) { case binop::Xor: diff --git a/src/ltlvisit/reduce.cc b/src/ltlvisit/reduce.cc index 9821705f2..eba5ac88c 100644 --- a/src/ltlvisit/reduce.cc +++ b/src/ltlvisit/reduce.cc @@ -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(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(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(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(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(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(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(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(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(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(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; } } diff --git a/src/ltlvisit/syntimpl.cc b/src/ltlvisit/syntimpl.cc index ab5fcaefb..6c3fc8213 100644 --- a/src/ltlvisit/syntimpl.cc +++ b/src/ltlvisit/syntimpl.cc @@ -96,8 +96,10 @@ namespace spot return; case unop::X: { - const unop* op = dynamic_cast(f); - if (op && op->op() == unop::X) + if (f->kind() != formula::UnOp) + return; + const unop* op = static_cast(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(f); - const unop* fu = dynamic_cast(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(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(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(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(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(f); - if (fb && fb->op() == f2->op() + if (f->kind() != formula::BinOp) + return false; + const binop* fb = static_cast(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(f2); - if (!f2b) + if (f2->kind() != formula::BinOp) return false; - return special_case(f2b); + return special_case(static_cast(f2)); } int @@ -307,11 +324,12 @@ namespace spot result_ = true; return; case unop::X: - { - const unop* op = dynamic_cast(f); - if (op && op->op() == unop::X) - result_ = syntactic_implication(f1, op->child()); - } + if (f->kind() == formula::UnOp) + { + const unop* op = static_cast(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(f); - const unop* fu = dynamic_cast(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(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(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(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(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(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(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; diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index e22957770..c01a69a30 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -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(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(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(uo->child()); + need_parent = (uo->child()->kind() == formula::Constant); if (full_parent_) need_parent = false; os_ << "X";