HAL
Classes | Variables
hal::SMT::ModelParser Namespace Reference

Classes

struct  ParserContext
 'ParserContext' refers to the data structure that stores parser results. More...
 

Variables

ParserContext parser_context
 
const auto NameAction = [](const auto& ctx) { parser_context.current_name = _attr(ctx); }
 
const auto SortAction = [](const auto& ctx) { parser_context.current_size = boost::fusion::at_c<0>(_attr(ctx)); }
 
const auto BinaryValueAction = [](const auto& ctx) { parser_context.current_value = "0b" + _attr(ctx); }
 
const auto HexValueAction = [](const auto& ctx) { parser_context.current_value = "0x" + _attr(ctx); }
 
const auto SignalAssigmentAction
 
const auto NameRule = (+x3::char_("0-9a-zA-Z_"))[NameAction]
 
const auto SortRule = (x3::lit("(_ BitVec ") >> +x3::digit >> x3::lit(")"))[SortAction]
 
const auto BinaryValueRule = (x3::lit("#b") >> +x3::char_("0-1"))[BinaryValueAction]
 
const auto HexValueRule = (x3::lit("#x") >> +x3::xdigit)[HexValueAction]
 
const auto ValueRule = BinaryValueRule | HexValueRule
 
const auto SignalAssignmentRule = (x3::lit("(define-fun") >> NameRule >> x3::lit("()") >> SortRule >> ValueRule >> x3::lit(")"))[SignalAssigmentAction]
 
const auto BOOLECTOR_MODEL_GRAMMAR = +(x3::lit("(model") >> +SignalAssignmentRule >> x3::lit(")"))
 
const auto Z3_MODEL_GRAMMAR = (x3::lit("(") >> (+SignalAssignmentRule) >> x3::lit(")")) | +(x3::lit("(model") >> +SignalAssignmentRule >> x3::lit(")"))
 

Variable Documentation

◆ BinaryValueAction

const auto hal::SMT::ModelParser::BinaryValueAction = [](const auto& ctx) { parser_context.current_value = "0b" + _attr(ctx); }

Definition at line 38 of file types.cpp.

◆ BinaryValueRule

const auto hal::SMT::ModelParser::BinaryValueRule = (x3::lit("#b") >> +x3::char_("0-1"))[BinaryValueAction]

Definition at line 64 of file types.cpp.

◆ BOOLECTOR_MODEL_GRAMMAR

const auto hal::SMT::ModelParser::BOOLECTOR_MODEL_GRAMMAR = +(x3::lit("(model") >> +SignalAssignmentRule >> x3::lit(")"))

Definition at line 81 of file types.cpp.

Referenced by hal::SMT::Model::parse().

◆ HexValueAction

const auto hal::SMT::ModelParser::HexValueAction = [](const auto& ctx) { parser_context.current_value = "0x" + _attr(ctx); }

Definition at line 40 of file types.cpp.

◆ HexValueRule

const auto hal::SMT::ModelParser::HexValueRule = (x3::lit("#x") >> +x3::xdigit)[HexValueAction]

Definition at line 68 of file types.cpp.

◆ NameAction

const auto hal::SMT::ModelParser::NameAction = [](const auto& ctx) { parser_context.current_name = _attr(ctx); }

Definition at line 34 of file types.cpp.

◆ NameRule

const auto hal::SMT::ModelParser::NameRule = (+x3::char_("0-9a-zA-Z_"))[NameAction]

Definition at line 55 of file types.cpp.

◆ parser_context

ParserContext hal::SMT::ModelParser::parser_context

Definition at line 31 of file types.cpp.

Referenced by hal::SMT::Model::parse().

◆ SignalAssigmentAction

const auto hal::SMT::ModelParser::SignalAssigmentAction
Initial value:
= [](const auto& ) {
const auto value = (parser_context.current_value.at(1) == 'b') ? strtoull(parser_context.current_value.substr(2, parser_context.current_value.length() - 2).c_str(), nullptr, 2)
: strtoull(parser_context.current_value.c_str(), nullptr, 0);
const auto size = strtoul(parser_context.current_size.c_str(), nullptr, 0);
parser_context.model.insert({parser_context.current_name, {value, size}});
}
hal::SMT::ModelParser::parser_context
ParserContext parser_context
Definition: types.cpp:31
hal::SMT::ModelParser::ParserContext::current_name
std::string current_name
stores the current name of a variable assignment
Definition: types.cpp:23
hal::SMT::ModelParser::ParserContext::current_value
std::string current_value
stores the current value of a variable assignment
Definition: types.cpp:27
hal::SMT::ModelParser::ParserContext::model
std::map< std::string, std::tuple< u64, u16 > > model
stores mapping from variables to its (1) value and (2) bit-size
Definition: types.cpp:20
hal::SMT::ModelParser::ParserContext::current_size
std::string current_size
stores the current size of a variable assignment
Definition: types.cpp:25

Definition at line 43 of file types.cpp.

◆ SignalAssignmentRule

const auto hal::SMT::ModelParser::SignalAssignmentRule = (x3::lit("(define-fun") >> NameRule >> x3::lit("()") >> SortRule >> ValueRule >> x3::lit(")"))[SignalAssigmentAction]

Definition at line 76 of file types.cpp.

◆ SortAction

const auto hal::SMT::ModelParser::SortAction = [](const auto& ctx) { parser_context.current_size = boost::fusion::at_c<0>(_attr(ctx)); }

Definition at line 36 of file types.cpp.

◆ SortRule

const auto hal::SMT::ModelParser::SortRule = (x3::lit("(_ BitVec ") >> +x3::digit >> x3::lit(")"))[SortAction]

Definition at line 59 of file types.cpp.

◆ ValueRule

const auto hal::SMT::ModelParser::ValueRule = BinaryValueRule | HexValueRule

Definition at line 70 of file types.cpp.

◆ Z3_MODEL_GRAMMAR

const auto hal::SMT::ModelParser::Z3_MODEL_GRAMMAR = (x3::lit("(") >> (+SignalAssignmentRule) >> x3::lit(")")) | +(x3::lit("(model") >> +SignalAssignmentRule >> x3::lit(")"))

Definition at line 86 of file types.cpp.

Referenced by hal::SMT::Model::parse().