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

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