69 typedef std::map<formula, int>
fv_map;
71 typedef std::map<int, formula>
vf_map;
79 enum var_type { anon = 0, var, acc };
87 typedef std::vector<bdd_info> bdd_info_map;
102 int register_proposition(
formula f,
const void* for_me);
104 template <
typename T>
107 return register_proposition(f, for_me.get());
117 int has_registered_proposition(
formula f,
const void* me);
119 template <
typename T>
122 return has_registered_proposition(f, for_me.get());
132 return var_map.at(f);
146 int register_acceptance_variable(formula f,
const void* for_me);
148 template <
typename T>
151 return register_acceptance_variable(f, for_me.get());
163 int register_anonymous_variables(
int n,
const void* for_me);
165 template <
typename T>
168 return register_anonymous_variables(n, for_me.get());
179 void register_all_variables_of(
const void* from_other,
const void* for_me);
181 template <
typename T>
183 std::shared_ptr<T> for_me)
185 register_all_variables_of(from_other, for_me.get());
188 template <
typename T>
192 register_all_variables_of(from_other.get(), for_me);
195 template <
typename T,
typename U>
197 std::shared_ptr<U> for_me)
199 register_all_variables_of(from_other.get(), for_me.get());
211 void register_all_propositions_of(
const void* from_other,
214 template <
typename T>
216 std::shared_ptr<T> for_me)
218 register_all_propositions_of(from_other, for_me.get());
221 template <
typename T>
225 register_all_propositions_of(from_other.get(), for_me);
228 template <
typename T,
typename U>
230 std::shared_ptr<U> for_me)
232 register_all_propositions_of(from_other.get(), for_me.get());
239 void unregister_all_my_variables(
const void* me);
243 void unregister_variable(
int var,
const void* me);
245 template <
typename T>
248 unregister_variable(var, me.get());
254 std::ostream& dump(std::ostream& os)
const;
267 void assert_emptiness()
const;
275 typedef std::shared_ptr<bdd_dict> bdd_dict_ptr;
277 inline bdd_dict_ptr make_bdd_dict()
279 return std::make_shared<bdd_dict>();
std::set< const void * > ref_set
BDD-variable reference counts.
Definition: bdddict.hh:77
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:189
void register_all_propositions_of(std::shared_ptr< T > from_other, const void *for_me)
Register the same propositions as another object.
Definition: bdddict.hh:222
void register_all_propositions_of(const void *from_other, std::shared_ptr< T > for_me)
Register the same propositions as another object.
Definition: bdddict.hh:215
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:246
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:196
int register_proposition(formula f, std::shared_ptr< T > for_me)
Register an atomic proposition.
Definition: bdddict.hh:105
int register_anonymous_variables(int n, std::shared_ptr< T > for_me)
Register anonymous BDD variables.
Definition: bdddict.hh:166
int register_acceptance_variable(formula f, std::shared_ptr< T > for_me)
Register an acceptance variable.
Definition: bdddict.hh:149
void register_all_propositions_of(std::shared_ptr< T > from_other, std::shared_ptr< U > for_me)
Register the same propositions as another object.
Definition: bdddict.hh:229
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:120
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:182