23#include <spot/twa/bdddict.hh>
32 bool synt_impl =
true,
33 bool event_univ =
true,
34 bool containment_checks =
false,
35 bool containment_checks_stronger =
false,
36 bool nenoform_stop_on_boolean =
false,
37 bool reduce_size_strictly =
false,
38 bool boolean_to_isop =
false,
39 bool favor_event_univ =
false,
40 bool keep_top_xor =
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),
50 keep_top_xor(keep_top_xor)
60 containment_checks =
true;
61 containment_checks_stronger =
true;
78 bool containment_checks;
79 bool containment_checks_stronger;
82 bool nenoform_stop_on_boolean;
86 bool reduce_size_strictly;
90 bool favor_event_univ;
97 unsigned containment_max_states = 0;
100 unsigned containment_max_ops = 16;
104 class tl_simplifier_cache;
113 bdd_dict_ptr dict = make_bdd_dict());
207 tl_simplifier_cache* cache_;
Definition: simplify.hh:29
Rewrite or simplify f in various ways.
Definition: simplify.hh:109
bool implication(formula f, formula g)
Check whether f implies g.
formula simplify(formula f)
formula boolean_to_isop(formula f)
Rewrite a Boolean formula f into as an irredundant sum of product.
bdd_dict_ptr get_dict() const
Return the bdd_dict used.
bool syntactic_implication(formula f, formula g)
Syntactic implication.
tl_simplifier_options & options()
bool are_equivalent(formula f, formula g)
check whether two formulae are equivalent.
void clear_caches()
Clear all caches.
void print_stats(std::ostream &os) const
Dump statistics about the caches.
formula star_normal_form(formula f)
Cached version of spot::star_normal_form().
bdd as_bdd(formula f)
Convert a Boolean formula as a BDD.
bool syntactic_implication_neg(formula f, formula g, bool right)
Syntactic implication with one negated argument.
formula negative_normal_form(formula f, bool negated=false)
void clear_as_bdd_cache()
Clear the as_bdd() cache.
Definition: automata.hh:26