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

* spot/twaalgos/ltl2tgba_fm.cc: Various micro-optimizations.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2019-10-29 18:00:24 +01:00
parent 65dbfb0ff5
commit 28efa37218
1 changed files with 58 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

98
spot/twaalgos/ltl2tgba_fm.cc
View file

@ -35,6 +35,7 @@
#include <spot/twaalgos/ltl2tgba_fm.hh> #include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twa/bddprint.hh> #include <spot/twa/bddprint.hh>
#include <spot/twaalgos/sccinfo.hh> #include <spot/twaalgos/sccinfo.hh>
#include <spot/priv/robin_hood.hh>
namespace spot namespace spot
{ {
@ -111,12 +112,13 @@ namespace spot
~ratexp_to_dfa(); ~ratexp_to_dfa();
protected: protected:
typedef std::pair<twa_graph_ptr, const namer*> labelled_aut; // Use robin_hood::pair because std::pair is not no-throw constructible
typedef robin_hood::pair<twa_graph_ptr, const namer*> labelled_aut;
labelled_aut translate(formula f); labelled_aut translate(formula f);
private: private:
translate_dict& dict_; translate_dict& dict_;
typedef std::unordered_map<formula, labelled_aut> f2a_t; typedef robin_hood::unordered_node_map<formula, labelled_aut> f2a_t;
std::vector<labelled_aut> automata_; std::vector<labelled_aut> automata_;
f2a_t f2a_; f2a_t f2a_;
}; };
@ -158,7 +160,7 @@ namespace spot
tl_simplifier* ls; tl_simplifier* ls;
mark_tools mt; mark_tools mt;
typedef bdd_dict::fv_map fv_map; typedef robin_hood::unordered_flat_map<formula, int> fv_map;
typedef std::vector<formula> vf_map; typedef std::vector<formula> vf_map;
fv_map next_map; ///< Maps "Next" variables to BDD variables fv_map next_map; ///< Maps "Next" variables to BDD variables
@ -173,7 +175,7 @@ namespace spot
bool single_acc; bool single_acc;
acc_cond& acc; acc_cond& acc;
// Map BDD variables to acceptance marks. // Map BDD variables to acceptance marks.
std::map<int, unsigned> bm; robin_hood::unordered_flat_map<int, unsigned> bm;
bool unambiguous; bool unambiguous;
enum translate_flags enum translate_flags
@ -214,9 +216,9 @@ namespace spot
bool has_marked:1; bool has_marked:1;
}; };
typedef typedef robin_hood::unordered_node_map
std::unordered_map<flagged_formula, translated, <flagged_formula, translated, flagged_formula_hash>
flagged_formula_hash> flagged_formula_to_bdd_map; flagged_formula_to_bdd_map;
private: private:
flagged_formula_to_bdd_map ltl_bdd_; flagged_formula_to_bdd_map ltl_bdd_;
@ -238,7 +240,7 @@ namespace spot
if (a == bddtrue) if (a == bddtrue)
return {}; return {};
assert(a != bddfalse); assert(a != bddfalse);
std::vector<unsigned> t; acc_cond::mark_t res = {};
do do
{ {
int v = bdd_var(a); int v = bdd_var(a);
@ -246,13 +248,13 @@ namespace spot
a = bdd_low(a); a = bdd_low(a);
if (h != bddfalse) if (h != bddfalse)
{ {
t.emplace_back(bm[v]); res.set(bm[v]);
if (a == bddfalse) if (a == bddfalse)
a = h; a = h;
} }
} }
while (a != bddtrue); while (a != bddtrue);
return acc_cond::mark_t(t.begin(), t.end()); return res;
} }
int int
@ -260,8 +262,7 @@ namespace spot
{ {
if (single_acc) if (single_acc)
{ {
int num = dict->register_acceptance_variable int num = dict->register_acceptance_variable(formula::tt(), this);
(formula::tt(), this);
a_set &= bdd_ithvar(num); a_set &= bdd_ithvar(num);
auto p = bm.emplace(num, 0U); auto p = bm.emplace(num, 0U);
@ -360,13 +361,13 @@ namespace spot
std::ostream& std::ostream&
dump(std::ostream& os) const dump(std::ostream& os) const
{ {
os << "Next Variables:" << std::endl; os << "Next Variables:\n";
for (auto& fi: next_map) for (auto& fi: next_map)
{ {
os << " " << fi.second << ": Next["; os << " " << fi.second << ": Next[";
print_psl(os, fi.first) << ']' << std::endl; print_psl(os, fi.first) << "]\n";
} }
os << "Shared Dict:" << std::endl; os << "Shared Dict:\n";
dict->dump(os); dict->dump(os);
return os; return os;
} }
@ -414,14 +415,31 @@ namespace spot
formula formula
conj_bdd_to_formula(bdd b, op o = op::And) const conj_bdd_to_formula(bdd b, op o = op::And) const
{ {
if (b == bddtrue)
return formula::tt();
if (b == bddfalse) if (b == bddfalse)
return formula::ff(); return formula::ff();
vec v; // Unroll the first loop of the next do/while loop so that we
while (b != bddtrue) // do not have to create v when b is not a conjunction.
formula res = var_to_formula(bdd_var(b));
bdd high = bdd_high(b);
if (high == bddfalse)
{ {
int var = bdd_var(b); res = formula::Not(res);
formula res = var_to_formula(var); b = bdd_low(b);
bdd high = bdd_high(b); }
else
{
assert(bdd_low(b) == bddfalse);
b = high;
}
if (b == bddtrue)
return res;
vec v{std::move(res)};
do
{
res = var_to_formula(bdd_var(b));
high = bdd_high(b);
if (high == bddfalse) if (high == bddfalse)
{ {
res = formula::Not(res); res = formula::Not(res);
@ -433,8 +451,9 @@ namespace spot
b = high; b = high;
} }
assert(b != bddfalse); assert(b != bddfalse);
v.emplace_back(res); v.emplace_back(std::move(res));
} }
while (b != bddtrue);
return formula::multop(o, std::move(v)); return formula::multop(o, std::move(v));
} }
@ -1727,15 +1746,15 @@ namespace spot
} }
private: private:
typedef std::unordered_map<formula, bool> pfl_map; typedef robin_hood::unordered_flat_map<formula, bool> pfl_map;
pfl_map pfl_; pfl_map pfl_;
}; };
class formula_canonizer final class formula_canonicalizer final
{ {
public: public:
formula_canonizer(translate_dict& d, formula_canonicalizer(translate_dict& d,
bool fair_loop_approx, bdd all_promises) bool fair_loop_approx, bdd all_promises)
: fair_loop_approx_(fair_loop_approx), : fair_loop_approx_(fair_loop_approx),
all_promises_(all_promises), all_promises_(all_promises),
d_(d) d_(d)
@ -1837,7 +1856,7 @@ namespace spot
} }
formula formula
canonize(formula f) canonicalize(formula f)
{ {
bool new_variable = false; bool new_variable = false;
bdd b = translate(f, &new_variable).symbolic; bdd b = translate(f, &new_variable).symbolic;
@ -1863,14 +1882,14 @@ namespace spot
// We do this because many formulae (such as `aR(bRc)' and // We do this because many formulae (such as `aR(bRc)' and
// `aR(bRc).(bRc)') are equivalent, and are trivially identified // `aR(bRc).(bRc)') are equivalent, and are trivially identified
// by looking at the set of successors. // by looking at the set of successors.
typedef std::unordered_map<bdd, formula, typedef robin_hood::unordered_node_map<bdd, formula,
bdd_hash> bdd_to_formula_map; bdd_hash> bdd_to_formula_map;
bdd_to_formula_map b2f_; bdd_to_formula_map b2f_;
// Map each formula to its associated bdd. This speed things up when // Map each formula to its associated bdd. This speed things up when
// the same formula is translated several times, which especially // the same formula is translated several times, which especially
// occurs when canonize() is called repeatedly inside exprop. // occurs when canonicalize() is called repeatedly inside exprop.
typedef std::unordered_map<formula, typedef robin_hood::unordered_node_map
translate_dict::translated> formula_to_bdd_map; <formula, translate_dict::translated> formula_to_bdd_map;
formula_to_bdd_map f2b_; formula_to_bdd_map f2b_;
possible_fair_loop_checker pflc_; possible_fair_loop_checker pflc_;
@ -1986,7 +2005,7 @@ namespace spot
return f.is_boolean(); return f.is_boolean();
}); });
formula_canonizer fc(d, fair_loop_approx, all_promises); formula_canonicalizer fc(d, fair_loop_approx, all_promises);
// These are used when atomic propositions are interpreted as // These are used when atomic propositions are interpreted as
// events. There are two kinds of events: observable events are // events. There are two kinds of events: observable events are
@ -2024,7 +2043,7 @@ namespace spot
// This is in case the initial state is equivalent to true... // This is in case the initial state is equivalent to true...
if (symb_merge) if (symb_merge)
f2 = fc.canonize(f2); f2 = fc.canonicalize(f2);
formulae_to_translate.insert(f2); formulae_to_translate.insert(f2);
a->set_init_state(namer->new_state(f2)); a->set_init_state(namer->new_state(f2));
@ -2135,7 +2154,7 @@ namespace spot
// If we already know a state with the same // If we already know a state with the same
// successors, use it in lieu of the current one. // successors, use it in lieu of the current one.
if (symb_merge) if (symb_merge)
dest = fc.canonize(dest); dest = fc.canonicalize(dest);
bdd conds = bdd_existcomp(label, d.var_set); bdd conds = bdd_existcomp(label, d.var_set);
bdd promises = bdd_existcomp(label, d.a_set); bdd promises = bdd_existcomp(label, d.a_set);
@ -2185,8 +2204,9 @@ namespace spot
bdd c = bddfalse; bdd c = bddfalse;
while (i != dests.end() && i->dest.is_tt()) while (i != dests.end() && i->dest.is_tt())
c |= i++->cond; c |= i++->cond;
for (; i != dests.end(); ++i) if (c != bddfalse)
i->cond -= c; for (; i != dests.end(); ++i)
i->cond -= c;
} }
// Create transitions in the automaton // Create transitions in the automaton
@ -2223,10 +2243,8 @@ namespace spot
} }
auto& acc = a->acc(); auto& acc = a->acc();
unsigned ns = a->num_states(); for (auto& e: a->edges())
for (unsigned s = 0; s < ns; ++s) e.acc = acc.comp(e.acc);
for (auto& t: a->out(s))
t.acc = acc.comp(t.acc);
acc.set_generalized_buchi(); acc.set_generalized_buchi();