spot 2.11.2.dev
simplify.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2011-2017, 2019, 2020 Laboratoire de Recherche et Developpement
3// de l'Epita (LRDE).
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <spot/tl/formula.hh>
23#include <bddx.h>
24#include <spot/twa/bdddict.hh>
25#include <iosfwd>
26
27namespace spot
28{
30 {
31 public:
32 tl_simplifier_options(bool basics = true,
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),
43 synt_impl(synt_impl),
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)
52 {
53 }
54
55 tl_simplifier_options(int level) :
56 tl_simplifier_options(false, false, false)
57 {
58 switch (level)
59 {
60 case 3:
61 containment_checks = true;
62 containment_checks_stronger = true;
63 SPOT_FALLTHROUGH;
64 case 2:
65 synt_impl = true;
66 SPOT_FALLTHROUGH;
67 case 1:
68 reduce_basics = true;
69 event_univ = true;
70 SPOT_FALLTHROUGH;
71 default:
72 break;
73 }
74 }
75
76 bool reduce_basics;
77 bool synt_impl;
78 bool event_univ;
79 bool containment_checks;
80 bool containment_checks_stronger;
81 // If true, Boolean subformulae will not be put into
82 // negative normal form.
83 bool nenoform_stop_on_boolean;
84 // If true, some rules that produce slightly larger formulae
85 // will be disabled. Those larger formulae are normally easier
86 // to translate, so we recommend to set this to false.
87 bool reduce_size_strictly;
88 // If true, Boolean subformulae will be rewritten in ISOP form.
89 bool boolean_to_isop;
90 // Try to isolate subformulae that are eventual and universal.
91 bool favor_event_univ;
92 // Keep Xor and Equiv at the top of the formula, possibly under
93 // &,|, and X operators. Only rewrite Xor and Equiv under
94 // temporal operators.
95 bool keep_top_xor;
96 // If greater than 0, bound the number of states used by automata
97 // in containment checks.
98 unsigned containment_max_states = 0;
99 };
100
101 // fwd declaration to hide technical details.
102 class tl_simplifier_cache;
103
106 class SPOT_API tl_simplifier
107 {
108 public:
109 tl_simplifier(const bdd_dict_ptr& dict = make_bdd_dict());
111 bdd_dict_ptr dict = make_bdd_dict());
113
117
118#ifndef SWIG
124#endif
125
134 formula
135 negative_normal_form(formula f, bool negated = false);
136
150 bool right);
151
157
158
165
171
182
187
189 bdd_dict_ptr get_dict() const;
190
193
200
202 void print_stats(std::ostream& os) const;
203
204 private:
205 tl_simplifier_cache* cache_;
206 // Copy disallowed.
207 tl_simplifier(const tl_simplifier&) = delete;
208 void operator=(const tl_simplifier&) = delete;
209 };
210}
Main class for temporal logic formula.
Definition: formula.hh:715
Definition: simplify.hh:30
Rewrite or simplify f in various ways.
Definition: simplify.hh:107
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.
LTL/PSL formula interface.
Definition: automata.hh:27

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.4