mCRL2
Loading...
Searching...
No Matches
mcrl2::smt Namespace Reference

Namespaces

namespace  detail
 

Classes

struct  always_false
 
class  child_process
 
struct  native_translations
 
class  smt_solver
 
class  stack_outstream
 
struct  structured_sort_functions
 Contains information on sorts that behave similar to a structured sort in a data specification. More...
 
class  translation_error
 

Typedefs

typedef std::function< void(data::data_expression, std::function< void(std::string)>, std::function< void(data::data_expression)>)> native_translation_t
 

Enumerations

enum  answer { UNSAT = 0 , UNKNOWN = 1 , SAT = 2 }
 

Functions

std::ostream & operator<< (std::ostream &out, const answer &a)
 
native_translations initialise_native_translation (const data::data_specification &dataspec)
 
template<typename T , typename OutputStream >
void translate_data_expression (const T &x, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)
 
template<typename T , typename OutputStream >
void translate_assertion (const T &x, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)
 
template<typename Container , typename OutputStream >
void translate_variable_declaration (const Container &vars, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)
 
template<typename T , typename OutputStream >
void translate_sort_expression (const T &x, OutputStream &o, const native_translations &nt, const std::map< data::structured_sort, std::string > &snm=detail::empty_name_map())
 
template<typename OutputStream >
void translate_data_specification (const data::data_specification &dataspec, OutputStream &o, std::unordered_map< data::data_expression, std::string > &c, const native_translations &nt)
 
template<typename Skip = always_false<data::function_symbol>>
std::pair< structured_sort_functions, std::map< data::function_symbol, data::data_equation_vector > > find_structured_sort_functions (const data::data_specification &dataspec, Skip skip=Skip())
 Find sorts that behave like a structured sort and the associated rewrite rules.
 
std::set< data::function_symbolcomplete_recognisers_projections (const data::data_specification &dataspec, native_translations &nt, structured_sort_functions &ssf)
 Complete the containers with recognisers and projections in ssf.
 
void unfold_pattern_matching (const data::data_specification &dataspec, native_translations &nt)
 
std::string translate_identifier (const std::string &id)
 
std::string translate_identifier (const core::identifier_string &id)
 
std::string translate_symbol (const data::function_symbol &f, const native_translations &nt)
 
std::string make_projection_name (const data::function_symbol &cons, std::size_t i, const native_translations &nt)
 
data::function_symbol make_projection_func (const data::function_symbol &cons, const data::sort_expression &arg_sort, std::size_t i, const native_translations &nt)
 
std::string make_recogniser_name (const data::function_symbol &cons, const native_translations &nt)
 
data::function_symbol make_recogniser_func (const data::function_symbol &cons, const native_translations &nt)
 
template<class T >
std::vector< T > topological_sort (std::map< T, std::set< T > > dependencies)
 

Typedef Documentation

◆ native_translation_t

typedef std::function<void(data::data_expression, std::function<void(std::string)>, std::function<void(data::data_expression)>)> mcrl2::smt::native_translation_t

Definition at line 19 of file native_translation.h.

Enumeration Type Documentation

◆ answer

Enumerator
UNSAT 
UNKNOWN 
SAT 

Definition at line 21 of file answer.h.

Function Documentation

◆ complete_recognisers_projections()

std::set< data::function_symbol > mcrl2::smt::complete_recognisers_projections ( const data::data_specification dataspec,
native_translations nt,
structured_sort_functions ssf 
)

Complete the containers with recognisers and projections in ssf.

Also sets native translations and build a set of all recognisers and projections in dataspec.

Definition at line 260 of file unfold_pattern_matching.h.

◆ find_structured_sort_functions()

template<typename Skip = always_false<data::function_symbol>>
std::pair< structured_sort_functions, std::map< data::function_symbol, data::data_equation_vector > > mcrl2::smt::find_structured_sort_functions ( const data::data_specification dataspec,
Skip  skip = Skip() 
)

Find sorts that behave like a structured sort and the associated rewrite rules.

Template Parameters
SkipUnary Boolean function type.
Parameters
dataspecThe data specification to consider
skipIf skip(f) is true then function symbol f will not be considered
Returns
A pair containing: (1) recogniser and projection function symbols for each structured sort and (2) a map that gives a list of equations for each function symbol.

Definition at line 90 of file unfold_pattern_matching.h.

◆ initialise_native_translation()

native_translations mcrl2::smt::initialise_native_translation ( const data::data_specification dataspec)

Definition at line 125 of file solver.cpp.

◆ make_projection_func()

data::function_symbol mcrl2::smt::make_projection_func ( const data::function_symbol cons,
const data::sort_expression arg_sort,
std::size_t  i,
const native_translations nt 
)
inline

Definition at line 66 of file utilities.h.

◆ make_projection_name()

std::string mcrl2::smt::make_projection_name ( const data::function_symbol cons,
std::size_t  i,
const native_translations nt 
)
inline

Definition at line 50 of file utilities.h.

◆ make_recogniser_func()

data::function_symbol mcrl2::smt::make_recogniser_func ( const data::function_symbol cons,
const native_translations nt 
)
inline

Definition at line 85 of file utilities.h.

◆ make_recogniser_name()

std::string mcrl2::smt::make_recogniser_name ( const data::function_symbol cons,
const native_translations nt 
)
inline

Definition at line 73 of file utilities.h.

◆ operator<<()

std::ostream & mcrl2::smt::operator<< ( std::ostream &  out,
const answer a 
)
inline

Definition at line 29 of file answer.h.

◆ topological_sort()

template<class T >
std::vector< T > mcrl2::smt::topological_sort ( std::map< T, std::set< T > >  dependencies)

Definition at line 92 of file utilities.h.

◆ translate_assertion()

template<typename T , typename OutputStream >
void mcrl2::smt::translate_assertion ( const T &  x,
OutputStream &  o,
std::unordered_map< data::data_expression, std::string > &  c,
const native_translations nt 
)

Definition at line 176 of file translate_expression.h.

◆ translate_data_expression()

template<typename T , typename OutputStream >
void mcrl2::smt::translate_data_expression ( const T &  x,
OutputStream &  o,
std::unordered_map< data::data_expression, std::string > &  c,
const native_translations nt 
)

Definition at line 170 of file translate_expression.h.

◆ translate_data_specification()

template<typename OutputStream >
void mcrl2::smt::translate_data_specification ( const data::data_specification dataspec,
OutputStream &  o,
std::unordered_map< data::data_expression, std::string > &  c,
const native_translations nt 
)

Definition at line 305 of file translate_specification.h.

◆ translate_identifier() [1/2]

std::string mcrl2::smt::translate_identifier ( const core::identifier_string id)
inline

Definition at line 37 of file utilities.h.

◆ translate_identifier() [2/2]

std::string mcrl2::smt::translate_identifier ( const std::string &  id)
inline

Definition at line 23 of file utilities.h.

◆ translate_sort_expression()

template<typename T , typename OutputStream >
void mcrl2::smt::translate_sort_expression ( const T &  x,
OutputStream &  o,
const native_translations nt,
const std::map< data::structured_sort, std::string > &  snm = detail::empty_name_map() 
)

Definition at line 96 of file translate_sort.h.

◆ translate_symbol()

std::string mcrl2::smt::translate_symbol ( const data::function_symbol f,
const native_translations nt 
)
inline

Definition at line 43 of file utilities.h.

◆ translate_variable_declaration()

template<typename Container , typename OutputStream >
void mcrl2::smt::translate_variable_declaration ( const Container &  vars,
OutputStream &  o,
std::unordered_map< data::data_expression, std::string > &  c,
const native_translations nt 
)

Definition at line 184 of file translate_expression.h.

◆ unfold_pattern_matching()

void mcrl2::smt::unfold_pattern_matching ( const data::data_specification dataspec,
native_translations nt 
)
inline

Definition at line 303 of file unfold_pattern_matching.h.