mcrl2::data::detail::Manipulator Class Reference

Base class for classes that provide functionality to modify or create terms. More...

#include <manipulator.h>

Public Member Functions
	Manipulator (const Info &a_info)
	Constructor initializing the rewriter and the field f_info.
data_expression	orient (const data_expression &a_term)
	Orients the term a_term such that all equations of the form t1 == t2 are.
data_expression	set_true (const data_expression &a_formula, const data_expression &a_guard) const
	Initializes the table Manipulator::f_set_true and calls.
data_expression	set_false (const data_expression &a_formula, const data_expression &a_guard) const
	Initializes the table Manipulator::f_set_false and calls the method.

Static Public Member Functions
static data_expression	make_reduced_if_then_else (const data_expression &a_expr, const data_expression &a_high, const data_expression &a_low)
	Returns an expression in the internal format of the rewriter with the jitty strategy.

Protected Member Functions
data_expression	set_true_auxiliary (const data_expression &a_formula, const data_expression &a_guard, std::unordered_map< data_expression, data_expression > &f_set_true) const
	Replaces all occurences of a_guard in a_formula by true. Additionally, if the variable.
data_expression	set_false_auxiliary (const data_expression &a_formula, const data_expression &a_guard, std::unordered_map< data_expression, data_expression > &f_set_false) const
	Replaces all occurences of a_guard in a_formula by false.

Protected Attributes
const Info &	f_info
	A class that provides information on the structure of expressions in one of the.
std::unordered_map< data_expression, data_expression >	f_orient
	A table used by the method Manipulator::orient. The method Manipulator::orient stores resulting terms in this table. If a term is encountered that has already been processed, it is not processed again, but retreived from this table.

Detailed Description

Base class for classes that provide functionality to modify or create terms.

Definition at line 22 of file manipulator.h.

Constructor & Destructor Documentation

Manipulator()

mcrl2::data::detail::Manipulator::Manipulator ( const Info &  a_info )

inline

Constructor initializing the rewriter and the field f_info.

Definition at line 146 of file manipulator.h.

Member Function Documentation

make_reduced_if_then_else()

static data_expression mcrl2::data::detail::Manipulator::make_reduced_if_then_else ( const data_expression &  a_expr, const data_expression &  a_high, const data_expression &  a_low  )

inlinestatic

Returns an expression in the internal format of the rewriter with the jitty strategy.

The main operator of this expression is an if then else function. Its guard is a_expr,

the true-branch is a_high and the false-branch is a_low. If a_high equals a_low, the

method returns a_high instead.

Definition at line 154 of file manipulator.h.

orient()

data_expression mcrl2::data::detail::Manipulator::orient ( const data_expression &  a_term )

inline

Orients the term a_term such that all equations of the form t1 == t2 are.

replaced by t2 == t1 if t1 > t2.

Definition at line 163 of file manipulator.h.

set_false()

data_expression mcrl2::data::detail::Manipulator::set_false ( const data_expression &  a_formula, const data_expression &  a_guard  ) const

inline

Initializes the table Manipulator::f_set_false and calls the method.

AM_Jitty::f_set_false_auxiliary.

Definition at line 211 of file manipulator.h.

set_false_auxiliary()

data_expression mcrl2::data::detail::Manipulator::set_false_auxiliary ( const data_expression &  a_formula, const data_expression &  a_guard, std::unordered_map< data_expression, data_expression > &  f_set_false  ) const

inlineprotected

Replaces all occurences of a_guard in a_formula by false.

Definition at line 98 of file manipulator.h.

set_true()

data_expression mcrl2::data::detail::Manipulator::set_true ( const data_expression &  a_formula, const data_expression &  a_guard  ) const

inline

Initializes the table Manipulator::f_set_true and calls.

f_set_true_auxiliary.

Definition at line 201 of file manipulator.h.

set_true_auxiliary()

data_expression mcrl2::data::detail::Manipulator::set_true_auxiliary ( const data_expression &  a_formula, const data_expression &  a_guard, std::unordered_map< data_expression, data_expression > &  f_set_true  ) const

inlineprotected

Replaces all occurences of a_guard in a_formula by true. Additionally, if the variable.

on the righthand side of the guard is encountered in a_formula, it is replaced by the variable

on the lefthand side.

Definition at line 38 of file manipulator.h.

Member Data Documentation

f_info

const Info& mcrl2::data::detail::Manipulator::f_info

protected

A class that provides information on the structure of expressions in one of the.

internal formats of the rewriter.

Definition at line 27 of file manipulator.h.

f_orient

std::unordered_map< data_expression, data_expression> mcrl2::data::detail::Manipulator::f_orient

protected

A table used by the method Manipulator::orient. The method Manipulator::orient stores resulting terms in this table. If a term is encountered that has already been processed, it is not processed again, but retreived from this table.

Definition at line 33 of file manipulator.h.

---

The documentation for this class was generated from the following file:

• data/include/mcrl2/data/detail/prover/manipulator.h