13#ifndef MCRL2_DATA_DETAIL_ENUMERATOR_ITERATION_LIMIT_H
14#define MCRL2_DATA_DETAIL_ENUMERATOR_ITERATION_LIMIT_H
38 enumerator_iteration_limit<std::size_t>::max_enumerator_iterations = size;
44 return enumerator_iteration_limit<std::size_t>::max_enumerator_iterations;
bool operator==(const unprotected_aterm_core &t) const
Comparison operator.
An abstraction expression.
const variable_list & variables() const
const data_expression & body() const
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.
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.
void rewrite_lambda_application(data_expression &result, const abstraction &lambda_term, const application &t, substitution_type &sigma)
void rewrite_where(data_expression &result, const where_clause &term, substitution_type &sigma)
void existential_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
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)
void universal_quantifier_enumeration(data_expression &result, const abstraction &t, substitution_type &sigma)
mutable_indexed_substitution substitution_type
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)
data_expression rewrite_lambda_application(const data_expression &t, substitution_type &sigma)
void rewrite_single_lambda(data_expression &result, const variable_list &vl, const data_expression &body, const bool body_in_normal_form, substitution_type &sigma)
void universal_quantifier_enumeration(data_expression &result, const variable_list &vl, const data_expression &t1, const bool t1_is_normal_form, substitution_type &sigma)
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)
An enumerator algorithm that generates solutions of a condition.
The default element for the todo list of the enumerator.
\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...
\brief A where expression
const assignment_list & assignments() const
const data_expression & body() const
logger(const log_level_t l)
Default constructor.
Standard exception class for reporting runtime errors.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
The main namespace for the aterm++ library.
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...
static void checkPattern(const data_expression &p)
static void check_vars(application::const_iterator begin, const application::const_iterator &end, const std::set< variable > &vars, std::set< variable > &used_vars)
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.
static bool occur_check(const variable &v, const atermpp::aterm &e)
static void checkPattern(application::const_iterator begin, const application::const_iterator &end)
static void check_vars(const data_expression &expr, const std::set< variable > &vars, std::set< variable > &used_vars)
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.
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_.
const function_symbol & false_()
Constructor for function symbol false.
const function_symbol & true_()
Constructor for function symbol true.
Namespace for all data library functionality.
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)
std::vector< variable > variable_vector
\brief vector of variables
std::string pp(const data::data_equation &x)
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
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)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
static std::size_t max_enumerator_iterations
bool operator()(const atermpp::aterm &t) const
rewriter_wrapper(Rewriter *r)
std::size_t operator()(const atermpp::detail::reference_aterm< T > &t) const