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;
103 template <
typename T>
106 return register_proposition(f, for_me.get());
118 template <
typename T>
121 return has_registered_proposition(f, for_me.get());
131 return var_map.at(f);
147 template <
typename T>
150 return register_acceptance_variable(f, for_me.get());
164 template <
typename T>
167 return register_anonymous_variables(n, for_me.get());
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());
211 template <
typename T>
214 unregister_variable(var, me.get());
220 std::ostream&
dump(std::ostream& os)
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>();
Map BDD variables to formulae.
Definition: bdddict.hh:56
std::set< const void * > ref_set
BDD-variable reference counts.
Definition: bdddict.hh:77
int register_acceptance_variable(formula f, const void *for_me)
Register an acceptance variable.
void assert_emptiness() const
Make sure the dictionary is empty.
std::ostream & dump(std::ostream &os) const
Dump all variables for debugging.
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
std::map< int, formula > vf_map
BDD-variable-to-formula maps.
Definition: bdddict.hh:71
std::map< formula, int > fv_map
Formula-to-BDD-variable maps.
Definition: bdddict.hh:69
void unregister_variable(int var, std::shared_ptr< T > me)
Release a variable used by me.
Definition: bdddict.hh:212
int register_proposition(formula f, const void *for_me)
Register an atomic proposition.
void unregister_all_my_variables(const void *me)
Release all variables used by an object.
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, const void *for_me)
Register anonymous BDD variables.
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
int has_registered_proposition(formula f, const void *me)
whether a proposition has already been registered
fv_map var_map
Maps atomic propositions to BDD variables.
Definition: bdddict.hh:73
void unregister_variable(int var, const void *me)
Release a variable used by me.
int register_anonymous_variables(int n, std::shared_ptr< T > for_me)
Register anonymous BDD variables.
Definition: bdddict.hh:165
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
fv_map acc_map
Maps acceptance conditions to BDD variables.
Definition: bdddict.hh:74
int register_acceptance_variable(formula f, std::shared_ptr< T > for_me)
Register an acceptance variable.
Definition: bdddict.hh:148
~bdd_dict()
Destroy the BDD dict.
void register_all_variables_of(const void *from_other, const void *for_me)
Duplicate the variable usage of another object.
Definition: automata.hh:27
Definition: bdddict.hh:80