69 typedef std::map<formula, int>
fv_map;
71 typedef std::map<int, formula>
vf_map;
79 enum var_type { anon = 0, var, acc };
86 typedef std::vector<bdd_info> bdd_info_map;
101 int register_proposition(
formula f,
const void* for_me);
103 template <
typename T>
106 return register_proposition(f, for_me.get());
116 int has_registered_proposition(
formula f,
const void* me);
118 template <
typename T>
121 return has_registered_proposition(f, for_me.get());
131 return var_map.at(f);
145 int register_acceptance_variable(
formula f,
const void* for_me);
147 template <
typename T>
150 return register_acceptance_variable(f, for_me.get());
162 int register_anonymous_variables(
int n,
const void* for_me);
164 template <
typename T>
167 return register_anonymous_variables(n, for_me.get());
178 void register_all_variables_of(
const void* from_other,
const void* for_me);
180 template <
typename T>
182 std::shared_ptr<T> for_me)
184 register_all_variables_of(from_other, for_me.get());
187 template <
typename T>
191 register_all_variables_of(from_other.get(), for_me);
194 template <
typename T,
typename U>
196 std::shared_ptr<U> for_me)
198 register_all_variables_of(from_other.get(), for_me.get());
205 void unregister_all_my_variables(
const void* me);
209 void unregister_variable(
int var,
const void* me);
211 template <
typename T>
214 unregister_variable(var, me.get());
220 std::ostream& dump(std::ostream& os)
const;
233 void assert_emptiness()
const;
241 typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
243 inline bdd_dict_ptr make_bdd_dict()
245 return std::make_shared<bdd_dict>();
std::set< const void * > ref_set
BDD-variable reference counts.
Definition: bdddict.hh:77
Definition: automata.hh:26
std::map< int, formula > vf_map
BDD-variable-to-formula maps.
Definition: bdddict.hh:71
fv_map acc_map
Maps acceptance conditions to BDD variables.
Definition: bdddict.hh:74
std::map< formula, int > fv_map
Formula-to-BDD-variable maps.
Definition: bdddict.hh:69
void register_all_variables_of(std::shared_ptr< T > from_other, const void *for_me)
Duplicate the variable usage of another object.
Definition: bdddict.hh:188
Definition: bdddict.hh:80
Map BDD variables to formulae.
Definition: bdddict.hh:55
void unregister_variable(int var, std::shared_ptr< T > me)
Release a variable used by me.
Definition: bdddict.hh:212
void register_all_variables_of(std::shared_ptr< T > from_other, std::shared_ptr< U > for_me)
Duplicate the variable usage of another object.
Definition: bdddict.hh:195
int register_proposition(formula f, std::shared_ptr< T > for_me)
Register an atomic proposition.
Definition: bdddict.hh:104
int register_anonymous_variables(int n, std::shared_ptr< T > for_me)
Register anonymous BDD variables.
Definition: bdddict.hh:165
int register_acceptance_variable(formula f, std::shared_ptr< T > for_me)
Register an acceptance variable.
Definition: bdddict.hh:148
fv_map var_map
Maps atomic propositions to BDD variables.
Definition: bdddict.hh:73
int has_registered_proposition(formula f, std::shared_ptr< T > for_me)
whether a proposition has already been registered
Definition: bdddict.hh:119
void register_all_variables_of(const void *from_other, std::shared_ptr< T > for_me)
Duplicate the variable usage of another object.
Definition: bdddict.hh:181