spot  2.12.1
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 
26 namespace 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());
114  ~tl_simplifier();
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 
172  bdd as_bdd(formula f);
173 
184 
188  void clear_caches();
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.
bool are_equivalent(formula f, formula g)
check whether two formulae are equivalent.
void clear_caches()
Clear all caches.
tl_simplifier_options & options()
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.1