Options controlling which simplification passes the tl_simplifier applies.
More...
#include <spot/tl/simplify.hh>
|
| | tl_simplifier_options (bool basics=true, bool synt_impl=true, bool event_univ=true, bool containment_checks=false, bool containment_checks_stronger=false, bool nenoform_stop_on_boolean=false, bool reduce_size_strictly=false, bool boolean_to_isop=false, bool favor_event_univ=false, bool keep_top_xor=false, bool unit_prop=false) |
| | Construct with individual option flags. More...
|
| |
| | tl_simplifier_options (int level) |
| | Construct from a simplification level (0–3). More...
|
| |
| bool | is_enabled () const |
| | Return true if any simplification option is enabled. More...
|
| |
| void | save_to_option_map (option_map &om, const char *prefix) const |
| |
| bool | load_from_option_map (const option_map &om, const char *prefix) |
| |
Options controlling which simplification passes the tl_simplifier applies.
◆ tl_simplifier_options() [1/2]
| spot::tl_simplifier_options::tl_simplifier_options |
( |
bool |
basics = true, |
|
|
bool |
synt_impl = true, |
|
|
bool |
event_univ = true, |
|
|
bool |
containment_checks = false, |
|
|
bool |
containment_checks_stronger = false, |
|
|
bool |
nenoform_stop_on_boolean = false, |
|
|
bool |
reduce_size_strictly = false, |
|
|
bool |
boolean_to_isop = false, |
|
|
bool |
favor_event_univ = false, |
|
|
bool |
keep_top_xor = false, |
|
|
bool |
unit_prop = false |
|
) |
| |
|
inline |
Construct with individual option flags.
◆ tl_simplifier_options() [2/2]
| spot::tl_simplifier_options::tl_simplifier_options |
( |
int |
level | ) |
|
|
inline |
Construct from a simplification level (0–3).
Level 0: no simplification; level 1: basics + event_univ; level 2: + synt_impl; level 3: + containment checks.
◆ is_enabled()
| bool spot::tl_simplifier_options::is_enabled |
( |
| ) |
const |
|
inline |
Return true if any simplification option is enabled.
◆ load_from_option_map()
| bool spot::tl_simplifier_options::load_from_option_map |
( |
const option_map & |
om, |
|
|
const char * |
prefix |
|
) |
| |
Load options from om with keys prefixed by prefix. Only keys that exist in om are updated; missing keys leave the corresponding field unchanged.
- Returns
- true if om contained at least one key with the given prefix.
◆ save_to_option_map()
| void spot::tl_simplifier_options::save_to_option_map |
( |
option_map & |
om, |
|
|
const char * |
prefix |
|
) |
| const |
Save this set of options into om with keys prefixed by prefix. All fields are stored as integers.
◆ boolean_to_isop
| bool spot::tl_simplifier_options::boolean_to_isop |
If true, Boolean subformulae will be rewritten in ISOP form.
◆ containment_checks
| bool spot::tl_simplifier_options::containment_checks |
Enable language containment checks.
◆ containment_checks_stronger
| bool spot::tl_simplifier_options::containment_checks_stronger |
Enable stronger containment checks.
◆ containment_max_ops
| unsigned spot::tl_simplifier_options::containment_max_ops = 16 |
If greater than 0, maximal number of terms in a multop to perform containment checks on this multop.
◆ containment_max_states
| unsigned spot::tl_simplifier_options::containment_max_states = 0 |
If greater than 0, bound the number of states used by automata in containment checks.
◆ event_univ
| bool spot::tl_simplifier_options::event_univ |
Enable eventuality/universality reductions.
◆ favor_event_univ
| bool spot::tl_simplifier_options::favor_event_univ |
Try to isolate subformulae that are eventual and universal.
◆ keep_top_xor
| bool spot::tl_simplifier_options::keep_top_xor |
Keep Xor and Equiv at the top of the formula, possibly under &,|, and X operators. Only rewrite Xor and Equiv under temporal operators.
◆ nenoform_stop_on_boolean
| bool spot::tl_simplifier_options::nenoform_stop_on_boolean |
If true, Boolean subformulae will not be put into negative normal form.
◆ reduce_basics
| bool spot::tl_simplifier_options::reduce_basics |
Enable basic rewriting rules.
◆ reduce_size_strictly
| bool spot::tl_simplifier_options::reduce_size_strictly |
If true, some rules that produce slightly larger formulas will be disabled. Those larger formulas are normally easier to translate, so we recommend to set this to false.
◆ synt_impl
| bool spot::tl_simplifier_options::synt_impl |
Enable syntactic implication simplifications.
◆ unit_prop
| bool spot::tl_simplifier_options::unit_prop |
Enable unit-propagation-based simplification (see spot::unit_propagate) as a first pass before recursive rewriting.
The documentation for this class was generated from the following file:
