24 #include <spot/twa/bdddict.hh> 33 bool synt_impl =
true,
34 bool event_univ =
true,
35 bool containment_checks =
false,
36 bool containment_checks_stronger =
false,
37 bool nenoform_stop_on_boolean =
false,
38 bool reduce_size_strictly =
false,
39 bool boolean_to_isop =
false,
40 bool favor_event_univ =
false)
41 : reduce_basics(basics),
43 event_univ(event_univ),
44 containment_checks(containment_checks),
45 containment_checks_stronger(containment_checks_stronger),
46 nenoform_stop_on_boolean(nenoform_stop_on_boolean),
47 reduce_size_strictly(reduce_size_strictly),
48 boolean_to_isop(boolean_to_isop),
49 favor_event_univ(favor_event_univ)
59 containment_checks =
true;
60 containment_checks_stronger =
true;
77 bool containment_checks;
78 bool containment_checks_stronger;
81 bool nenoform_stop_on_boolean;
85 bool reduce_size_strictly;
89 bool favor_event_univ;
93 class tl_simplifier_cache;
102 bdd_dict_ptr dict = make_bdd_dict());
177 void clear_as_bdd_cache();
185 bdd_dict_ptr get_dict()
const;
198 void print_stats(std::ostream& os)
const;
201 tl_simplifier_cache* cache_;
Definition: simplify.hh:29
Rewrite or simplify f in various ways.
Definition: simplify.hh:97
formula negative_normal_form(formula f, bool negated=false)
Build the negative normal form of f.