Commit 9a14d28a authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Use bdd_satprefix() to speedup minato on BDDs that are almost cubes.

* src/misc/minato.cc (minato_isop::minato_isop): Call bdd_satprefix.
(minato_isop::next): Avoid useless intermediate variables.
* src/misc/minato.hh: Typo in comments.
parent 253ee350
2009-11-23 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Use bdd_satprefix() to speedup minato on BDDs that are almost cubes.
* src/misc/minato.cc (minato_isop::minato_isop): Call bdd_satprefix.
(minato_isop::next): Avoid useless intermediate variables.
* src/misc/minato.hh: Typo in comments.
2009-11-23 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Specialize scc_filter when handling tgba_explicit_formula automata.
......
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris
// 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
......@@ -20,7 +20,6 @@
// 02111-1307, USA.
#include "minato.hh"
#include <utility>
#include <cassert>
namespace spot
......@@ -30,15 +29,22 @@ namespace spot
: ret_(bddfalse)
{
// If INPUT has the form a&b&c&(binary function) we want to
// compute the ISOP of the only binary and prepend a&b&c latter.
//
// Calling bdd_satprefix (it returns a&b&c and modify input to
// point to function) this way is an optimization to the
// original algorithm, because in many cases we are trying to
// build ISOPs out of formulae that are already cubes.
cube_.push(bdd_satprefix(input));
todo_.push(local_vars(input, input, bdd_support(input)));
cube_.push(bddtrue);
}
minato_isop::minato_isop(bdd input, bdd vars)
: ret_(bddfalse)
{
cube_.push(bdd_satprefix(input));
todo_.push(local_vars(input, input, vars));
cube_.push(bddtrue);
}
bdd
......@@ -138,10 +144,8 @@ namespace spot
l.g1 = ret_;
cube_.pop();
{
bdd f0s_min = l.f0_min - l.g0;
bdd f1s_min = l.f1_min - l.g1;
bdd fs_max = l.f0_max & l.f1_max;
bdd fs_min = fs_max & (f0s_min | f1s_min);
bdd fs_min = fs_max & ((l.f0_min - l.g0) | (l.f1_min - l.g1));
todo_.push(local_vars(fs_min, fs_max, l.vars));
}
continue;
......
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// Copyright (C) 2003, 2004, 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
......@@ -65,17 +65,17 @@ namespace spot
/// Internal variables for minato_isop.
struct local_vars
{
// If you are following the paper, f_min and f_max corresponds
// to the pair of BDD function used to encode the ternary function `f'
// If you are following the paper, f_min and f_max correspond
// to the pair of BDD functions used to encode the ternary function f
// (see Section 3.4).
// Also note that f0, f0', and f0'' all share the same _max function.
// Likewise for f1, f1', and f1''.
bdd f_min, f_max;
// Because we need a non-recursive version of the algorithm,
// we had to split it in four step (each step is separated
// we had to split it in four steps (each step is separated
// from the other by a call to ISOP in the original algorithm).
enum { FirstStep, SecondStep, ThirdStep, FourthStep } step;
// The list of variable to factorize. This is an addition to
// The list of variables to factorize. This is an addition to
// the original algorithm.
bdd vars;
bdd v1;
......
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