mCRL2
Loading...
Searching...
No Matches
data2pbes_rewriter.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
11
12#ifndef MCRL2_PBES_REWRITERS_DATA2PBES_REWRITER_H
13#define MCRL2_PBES_REWRITERS_DATA2PBES_REWRITER_H
14
16#include "mcrl2/pbes/builder.h"
17
18namespace mcrl2 {
19
20namespace pbes_system {
21
22namespace detail {
23
24// transforms outer level data operators to their pbes equivalents, for the following operators:
25// x && y
26// x || y
27// x => y
28// exists d:D. x
29// forall d:D. x
30template <typename Derived>
32{
34 using super::apply;
35
36 bool is_not(const data::data_expression& x) const
37 {
38 return data::is_not(x);
39 }
40
41 bool is_and(const data::data_expression& x) const
42 {
43 return data::is_and(x);
44 }
45
46 bool is_or(const data::data_expression& x) const
47 {
48 return data::is_or(x);
49 }
50
51 bool is_imp(const data::data_expression& x) const
52 {
53 return data::is_imp(x);
54 }
55
56 bool is_forall(const data::data_expression& x) const
57 {
58 return data::is_forall(x);
59 }
60
61 bool is_exists(const data::data_expression& x) const
62 {
63 return data::is_exists(x);
64 }
65
67 {
68 return data::unary_operand(atermpp::down_cast<data::application>(x));
69 }
70
72 {
73 return data::binary_left(atermpp::down_cast<data::application>(x));
74 }
75
77 {
78 return data::binary_right(atermpp::down_cast<data::application>(x));
79 }
80
81 // transforms outer level data operators to their pbes equivalents, for the following operators:
82 // !x
83 // x && y
84 // x || y
85 // x => y
86 // exists d:D. x
87 // forall d:D. x
89 {
90 if (is_not(x))
91 {
92 return not_(data2pbes(operand(x)));
93 }
94 else if (is_and(x))
95 {
96 return and_(data2pbes(left(x)), data2pbes(right(x)));
97 }
98 else if (is_or(x))
99 {
100 return or_(data2pbes(left(x)), data2pbes(right(x)));
101 }
102 else if (is_imp(x))
103 {
104 return imp(data2pbes(left(x)), data2pbes(right(x)));
105 }
106 else if (is_forall(x))
107 {
108 data::forall y(x);
109 return forall(y.variables(), data2pbes(y.body()));
110 }
111 else if (is_exists(x))
112 {
113 data::exists y(x);
114 return exists(y.variables(), data2pbes(y.body()));
115 }
116 return x;
117 }
118
119 template <class T>
120 void apply(T& result, const data::data_expression& x)
121 {
122 result = data2pbes(x);
123 }
124};
125
126template <typename T>
127T data2pbes(const T& x,
128 typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
129 )
130{
131 T result;
132 core::make_apply_builder<data2pbes_builder>().apply(result, x);
133 return result;
134}
135
136template <typename T>
137void data2pbes(T& x,
138 typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
139 )
140{
141 core::make_apply_builder<data2pbes_builder>().update(x);
142}
143
144} // namespace detail
145
148{
149 public:
152
155
160 {
161 return detail::data2pbes(x);
162 }
163};
164
165} // namespace pbes_system
166
167} // namespace mcrl2
168
169#endif // MCRL2_PBES_REWRITERS_DATA2PBES_REWRITER_H
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
existential quantification.
Definition exists.h:26
universal quantification.
Definition forall.h:26
\brief A data variable
Definition variable.h:28
\brief The and operator for pbes expressions
A rewriter that applies one point rule quantifier elimination to a PBES.
pbes_expression term_type
The term type.
pbes_expression operator()(const pbes_expression &x) const
Rewrites a pbes expression.
data::variable variable_type
The variable type.
\brief The existential quantification operator for pbes expressions
\brief The universal quantification operator for pbes expressions
\brief The implication operator for pbes expressions
\brief The not operator for pbes expressions
\brief The or operator for pbes expressions
This file contains some functions that are present in all libraries except the data library....
const data_expression & binary_right(const application &x)
bool is_exists(const atermpp::aterm_appl &x)
Returns true if the term t is an existential quantification.
bool is_or(const data_expression &x)
Test if x is a disjunction.
Definition consistency.h:53
const data_expression & unary_operand(const application &x)
bool is_not(const data_expression &x)
Test if x is a negation.
Definition consistency.h:45
const data_expression & binary_left(const application &x)
bool is_imp(const data_expression &x)
Test if x is an implication.
Definition consistency.h:69
bool is_forall(const atermpp::aterm_appl &x)
Returns true if the term t is a universal quantification.
bool is_and(const data_expression &x)
Test if x is a conjunction.
Definition consistency.h:61
T data2pbes(const T &x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
add your file description here.
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
Definition builder.h:544
pbes_expression_builder< Derived > super
data::data_expression left(const data::data_expression &x) const
bool is_not(const data::data_expression &x) const
pbes_expression data2pbes(const data::data_expression &x) const
void apply(T &result, const data::data_expression &x)
bool is_forall(const data::data_expression &x) const
bool is_exists(const data::data_expression &x) const
bool is_imp(const data::data_expression &x) const
data::data_expression operand(const data::data_expression &x) const
bool is_and(const data::data_expression &x) const
bool is_or(const data::data_expression &x) const
data::data_expression right(const data::data_expression &x) const