bdddict.hh 4.52 KB
Newer Older
1
2
3
#ifndef SPOT_TGBA_BDDDICT_HH
# define SPOT_TGBA_BDDDICT_HH

4
#include "misc/hash.hh"
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
#include <list>
#include <set>
#include <iostream>
#include <bdd.h>
#include "ltlast/formula.hh"
#include "misc/bddalloc.hh"

namespace spot
{

  /// Map BDD variables to formulae.
  class bdd_dict: public bdd_allocator
  {
  public:

    bdd_dict();
    ~bdd_dict();

    /// Formula-to-BDD-variable maps.
24
25
    typedef Sgi::hash_map<const ltl::formula*, int,
			  ptr_hash<ltl::formula> > fv_map;
26
    /// BDD-variable-to-formula maps.
27
    typedef Sgi::hash_map<int, const ltl::formula*> vf_map;
28
29
30

    fv_map now_map;		///< Maps formulae to "Now" BDD variables
    vf_map now_formula_map;	///< Maps "Now" BDD variables to formulae
31
32
    fv_map var_map;		///< Maps atomic propositions to BDD variables
    vf_map var_formula_map;     ///< Maps BDD variables to atomic propositions
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
    fv_map acc_map;		///< Maps accepting conditions to BDD variables
    vf_map acc_formula_map;	///< Maps BDD variables to accepting conditions

    /// \brief Map Next variables to Now variables.
    ///
    /// Use with BuDDy's bdd_replace() function.
    bddPair* next_to_now;
    /// \brief Map Now variables to Next variables.
    ///
    /// Use with BuDDy's bdd_replace() function.
    bddPair* now_to_next;

    /// \brief Register an atomic proposition.
    ///
    /// Return (and maybe allocate) a BDD variable designating formula
    /// \a f.  The \a for_me argument should point to the object using
    /// this BDD variable, this is used for reference counting.  It is
    /// perfectly safe to call this function several time with the same
    /// arguments.
    ///
    /// \return The variable number.  Use bdd_ithvar() or bdd_nithvar()
    ///   to convert this to a BDD.
    int register_proposition(const ltl::formula* f, const void* for_me);

    /// \brief Register a couple of Now/Next variables
    ///
    /// Return (and maybe allocate) two BDD variables for a state
    /// associated to formula \a f.  The \a for_me argument should point
    /// to the object using this BDD variable, this is used for
    /// reference counting.  It is perfectly safe to call this
    /// function several time with the same arguments.
    ///
    /// \return The first variable number.  Add one to get the second
    /// variable.  Use bdd_ithvar() or bdd_nithvar() to convert this
    /// to a BDD.
    int register_state(const ltl::formula* f, const void* for_me);

    /// \brief Register an atomic proposition.
    ///
    /// Return (and maybe allocate) a BDD variable designating an
    /// accepting set associated to formula \a f.  The \a for_me
    /// argument should point to the object using this BDD variable,
    /// this is used for reference counting.  It is perfectly safe to
    /// call this function several time with the same arguments.
    ///
    /// \return The variable number.  Use bdd_ithvar() or bdd_nithvar()
    ///   to convert this to a BDD.
    int register_accepting_variable(const ltl::formula* f, const void* for_me);

    /// \brief Duplicate the variable usage of another object.
    ///
    /// This tells this dictionary that the \a for_me object
    /// will be using the same BDD variables as the \a from_other objects.
    /// This ensure that the variables won't be freed when \a from_other
    /// is deleted if \a from_other is still alive.
    void register_all_variables_of(const void* from_other, const void* for_me);

    /// \brief Release the variables used by object.
    ///
    /// Usually called in the destructor if \a me.
    void unregister_all_my_variables(const void* me);

95
    /// @{
96
    /// Check whether formula \a f has already been registered by \a by_me.
97
98
99
100
101
    bool is_registered_proposition(const ltl::formula* f, const void* by_me);
    bool is_registered_state(const ltl::formula* f, const void* by_me);
    bool is_registered_accepting_variable(const ltl::formula* f,
					  const void* by_me);
    /// @}
102
103
104
105
106
107
108
109
110
111
112
113
114

    /// \brief Dump all variables for debugging.
    /// \param os The output stream.
    std::ostream& dump(std::ostream& os) const;

    /// \brief Make sure the dictionary is empty.
    ///
    /// This will print diagnostics and abort if the dictionary
    /// is not empty.  Use for debugging.
    void assert_emptiness() const;

  protected:
    /// BDD-variable reference counts.
115
116
    typedef Sgi::hash_set<const void*, ptr_hash<void> > ref_set;
    typedef Sgi::hash_map<int, ref_set> vr_map;
117
118
119
120
121
122
123
124
125
126
127
128
    vr_map var_refs;

  private:
    // Disallow copy.
    bdd_dict(const bdd_dict& other);
    bdd_dict& operator=(const bdd_dict& other);
  };


}

#endif // SPOT_TGBA_BDDDICT_HH