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 bool keep_top_xor =
false)
42 : reduce_basics(basics),
44 event_univ(event_univ),
45 containment_checks(containment_checks),
46 containment_checks_stronger(containment_checks_stronger),
47 nenoform_stop_on_boolean(nenoform_stop_on_boolean),
48 reduce_size_strictly(reduce_size_strictly),
49 boolean_to_isop(boolean_to_isop),
50 favor_event_univ(favor_event_univ),
51 keep_top_xor(keep_top_xor)
61 containment_checks =
true;
62 containment_checks_stronger =
true;
79 bool containment_checks;
80 bool containment_checks_stronger;
83 bool nenoform_stop_on_boolean;
87 bool reduce_size_strictly;
91 bool favor_event_univ;
99 class tl_simplifier_cache;
108 bdd_dict_ptr dict = make_bdd_dict());
178 void clear_as_bdd_cache();
186 bdd_dict_ptr get_dict()
const;
199 void print_stats(std::ostream& os)
const;
202 tl_simplifier_cache* cache_;
Definition: automata.hh:26
formula star_normal_form(formula sere, snf_cache *cache=nullptr)
Helper to rewrite a sere in Star Normal Form.
bool are_equivalent(const_twa_graph_ptr left, const_twa_graph_ptr right)
Test if the language of left is equivalent to that of right.
Definition: simplify.hh:29
Rewrite or simplify f in various ways.
Definition: simplify.hh:103
formula negative_normal_form(formula f, bool negated=false)
Build the negative normal form of f.