mCRL2
Loading...
Searching...
No Matches
enumerator_iteration_limit.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//
9/// \file mcrl2/data/detail/enumerator_iteration_limit.h
10/// \brief Stores a static variable that indicates the number of iterations
11/// allowed during enumeration
12
13#ifndef MCRL2_DATA_DETAIL_ENUMERATOR_ITERATION_LIMIT_H
14#define MCRL2_DATA_DETAIL_ENUMERATOR_ITERATION_LIMIT_H
15
16#include <cstddef>
17
18namespace mcrl2 {
19
20namespace data {
21
22namespace detail {
23
24// Stores the maximum number of iterations that may be performed during enumeration.
25template <class T> // note, T is only a dummy
27{
29};
30
31// Initialization
32template <class T>
34
35inline
37{
38 enumerator_iteration_limit<std::size_t>::max_enumerator_iterations = size;
39}
40
41inline
43{
44 return enumerator_iteration_limit<std::size_t>::max_enumerator_iterations;
45}
46
47} // namespace detail
48
49} // namespace data
50
51} // namespace mcrl2
52
53#endif // MCRL2_DATA_DETAIL_ENUMERATOR_ITERATION_LIMIT_H
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
Definition aterm_core.h:83
An abstraction expression.
Definition abstraction.h:26
const variable_list & variables() const
Definition abstraction.h:63
const data_expression & body() const
Definition abstraction.h:68
\brief A data equation
const data_expression & lhs() const
const variable_list & variables() const
data_expression & operator=(const data_expression &) noexcept=default
data_expression(const atermpp::aterm &term)
Rewriter interface class.
Definition rewrite.h:42
void rewrite_lambda_application(data_expression &result, const data_expression &t, substitution_type &sigma)
Rewrite t, assuming that the headsymbol of t, which can be nested, is a lambda term.
Definition rewrite.cpp:214
void rewrite_lambda_application(data_expression &result, const abstraction &lambda_term, const application &t, substitution_type &sigma)
Definition rewrite.cpp:256
void rewrite_where(data_expression &result, const where_clause &term, substitution_type &sigma)
Definition rewrite.cpp:70
void existential_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
Definition rewrite.cpp:334
virtual void rewrite(data_expression &result, const data_expression &term, substitution_type &sigma)=0
Rewrite an mCRL2 data term.
void existential_quantifier_enumeration(data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
Definition rewrite.cpp:350
void universal_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
Definition rewrite.cpp:362
mutable_indexed_substitution substitution_type
Definition rewrite.h:55
virtual data_expression rewrite(const data_expression &term, substitution_type &sigma)=0
Rewrite an mCRL2 data term.
data_expression rewrite_where(const where_clause &term, substitution_type &sigma)
Definition rewrite.cpp:61
data_expression rewrite_lambda_application(const data_expression &t, substitution_type &sigma)
Definition rewrite.cpp:241
void rewrite_single_lambda(data_expression &result, const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
Definition rewrite.cpp:109
void universal_quantifier_enumeration(data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
Definition rewrite.cpp:375
void quantifier_enumeration(data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma, const binder_type &binder, data_expression(*lazy_op)(const data_expression &, const data_expression &), const data_expression &identity_element, const data_expression &absorbing_element)
Definition rewrite.cpp:386
An enumerator algorithm that generates solutions of a condition.
Definition enumerator.h:601
The default element for the todo list of the enumerator.
Definition enumerator.h:231
\brief Binder for existential quantification
exists_binder()
\brief Default constructor X3.
\brief Binder for universal quantification
forall_binder()
\brief Default constructor X3.
\brief Binder for lambda abstraction
lambda_binder()
\brief Default constructor X3.
Component for selecting a subset of equations that are actually used in an encompassing specification...
Definition selection.h:37
\brief A data variable
Definition variable.h:28
\brief A where expression
const assignment_list & assignments() const
const data_expression & body() const
logger(const log_level_t l)
Default constructor.
Definition logger.h:164
Standard exception class for reporting runtime errors.
Definition exception.h:27
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:391
The main namespace for the aterm++ library.
Definition algorithm.h:21
void CheckRewriteRule(const data_equation &data_eqn)
Check that an mCRL2 data equation is a valid rewrite rule. If not, an runtime_error is thrown indicat...
Definition rewrite.cpp:597
static void checkPattern(const data_expression &p)
Definition rewrite.cpp:582
static void check_vars(application::const_iterator begin, const application::const_iterator &end, const std::set< variable > &vars, std::set< variable > &used_vars)
Definition rewrite.cpp:539
void set_enumerator_iteration_limit(std::size_t size)
bool isValidRewriteRule(const data_equation &data_eqn)
Check whether or not an mCRL2 data equation is a valid rewrite rule.
Definition rewrite.cpp:655
static bool occur_check(const variable &v, const atermpp::aterm &e)
Definition rewrite.cpp:44
static void checkPattern(application::const_iterator begin, const application::const_iterator &end)
Definition rewrite.cpp:573
static void check_vars(const data_expression &expr, const std::set< variable > &vars, std::set< variable > &used_vars)
Definition rewrite.cpp:550
std::shared_ptr< detail::Rewriter > createRewriter(const data_specification &DataSpec, const used_data_equation_selector &equations_selector, const rewrite_strategy Strategy=jitty)
Create a rewriter.
Definition rewrite.cpp:513
std::size_t get_enumerator_iteration_limit()
A collection of utilities for lazy expression construction.
data_expression and_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p or q.
data_expression or_(data_expression const &p, data_expression const &q)
Returns an expression equivalent to p and q.
Namespace for system defined sort bool_.
Definition bool.h:32
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
Namespace for all data library functionality.
Definition data.cpp:22
bool is_application(const data_expression &t)
Returns true if the term t is an application.
std::string pp(const rewrite_strategy s)
Pretty prints a rewrite strategy.
std::string pp(const data::variable &x)
Definition data.cpp:81
std::vector< variable > variable_vector
\brief vector of variables
Definition variable.h:89
std::string pp(const data::data_equation &x)
Definition data.cpp:51
rewrite_strategy
The strategy of the rewriter.
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
atermpp::term_list< variable > variable_list
\brief list of variables
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
atermpp::term_list< assignment > assignment_list
\brief list of assignments
Definition assignment.h:146
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
std::string pp(const data::data_expression &x)
Definition data.cpp:52
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
bool operator()(const atermpp::aterm &t) const
Definition rewrite.cpp:37
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const