alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Move language containment into ltl_simplifier.

Browse source 
* src/ltlvisit/simplify.cc: Integrate the tau03
containment rules.
* src/ltlvisit/simplify.hh: Add options to select simplifications.
* src/ltlvisit/reduce.cc (reduce): Do not call reduce_tau03().
* src/ltlvisit/contain.cc (reduce_tau03_visitor): Remove.
(reduce_tau03): Implement it using ltl_simplifier.
This commit is contained in:
Alexandre Duret-Lutz 2011-08-24 15:54:06 +02:00
parent 82b42494db
commit 1087c62356
4 changed files with 442 additions and 539 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ltlvisit/simplify.hh
View file

@ -31,15 +31,20 @@ namespace spot
class ltl_simplifier_options
{
public:
ltl_simplifier_options()
: reduce_basics(true),
synt_impl(true),
event_univ(true),
containment_checks(false),
containment_checks_stronger(false),
ltl_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)
: reduce_basics(basics),
synt_impl(synt_impl),
event_univ(event_univ),
containment_checks(containment_checks),
containment_checks_stronger(containment_checks_stronger),
// If true, Boolean subformulae will not be put into
// negative normal form.
nenoform_stop_on_boolean(false)
nenoform_stop_on_boolean(nenoform_stop_on_boolean)
{
}
@ -48,6 +53,8 @@ namespace spot
bool event_univ;
bool containment_checks;
bool containment_checks_stronger;
// If true, Boolean subformulae will not be put into
// negative normal form.
bool nenoform_stop_on_boolean;
};