Commit 484ea488 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Use bdd_implies() to speedup various algorithms.

* src/ltlvisit/simplify.cc, src/tgba/tgbaproduct.cc,
src/tgba/tgbatba.cc, src/tgbaalgos/sccfilter.cc,
src/tgbaalgos/simulation.cc: Here.
parent 821d5e54
......@@ -4140,15 +4140,9 @@ namespace spot
bool result;
if (f->is_boolean() && g->is_boolean())
{
bdd l = as_bdd(f);
bdd r = as_bdd(g);
result = ((l & r) == l);
}
result = bdd_implies(as_bdd(f), as_bdd(g));
else
{
result = syntactic_implication_aux(f, g);
}
result = syntactic_implication_aux(f, g);
// Cache result
{
......
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
// Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie.
......@@ -319,7 +319,7 @@ namespace spot
{
assert(bdd_high(tmp) == bddfalse);
int var = bdd_var(tmp);
if ((bdd_nithvar(var) & rna) == rna)
if (bdd_implies(rna, bdd_nithvar(var)))
{
int varclone = dict_->register_clone_acc(var, this);
bdd_setpair(right_common_acc_, var, varclone);
......
......@@ -241,11 +241,11 @@ namespace spot
--prev;
bdd common = aut->
common_acceptance_conditions_of_original_state(rs);
if ((common & *prev) == *prev)
if (bdd_implies(*prev, common))
{
bdd u = aut->
union_acceptance_conditions_of_original_state(odest);
if ((u & *prev) != *prev)
if (!bdd_implies(*prev, u))
acc -= *prev;
}
}
......@@ -279,7 +279,7 @@ namespace spot
// acceptance sets common to the outgoing transition of
// the destination state.
acc |= otheracc;
while (next != cycle.end() && (acc & *next) == *next)
while (next != cycle.end() && bdd_implies(*next, acc))
++next;
if (next != cycle.end())
{
......@@ -291,7 +291,7 @@ namespace spot
accepting = true;
// Skip as much acceptance conditions as we can on our cycle.
next = cycle.begin();
while (next != expected && (acc & *next) == *next)
while (next != expected && bdd_implies(*next, acc))
++next;
next_is_set:
state_tba_proxy* dest =
......
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
......@@ -142,8 +142,7 @@ namespace spot
// and we want to find that 'a' and 'b' are useless because
// they always occur with 'c'.
// The way we check if 'a' is useless that is to look whether
// USEFUL & (x -> a) == USEFUL for some other acceptance
// condition x.
// USEFUL implies (x -> a) for some other acceptance condition x.
bdd allconds = bdd_support(negall);
bdd allcondscopy = allconds;
bdd useless = bddtrue;
......@@ -157,7 +156,7 @@ namespace spot
bdd x = bdd_ithvar(bdd_var(others));
if (x != a)
{
if ((useful & (x >> a)) == useful)
if (bdd_implies(useful, x >> a))
{
// a is useless
useful = bdd_exist(useful, a);
......
......@@ -411,8 +411,7 @@ namespace spot
if (it1 == it2)
continue;
// We detect that "a&b -> a" by testing "a&b = a".
if ((it1->first & it2->first) == (it1->first))
if (bdd_implies(it1->first, it2->first))
{
accu &= it2->second;
++po_size_;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment