types.cpp File Reference

#include "hal_core/netlist/boolean_function/types.h"
#include <boost/spirit/home/x3.hpp>
#include <mutex>
#include <numeric>
#include <sstream>

Include dependency graph for types.cpp:

Go to the source code of this file.

Classes
struct	hal::SMT::ModelParser::ParserContext
	'ParserContext' refers to the data structure that stores parser results. More...

Namespaces
	hal
	hal::SMT
	hal::SMT::ModelParser

Functions
std::ostream &	hal::SMT::operator<< (std::ostream &out, const QueryConfig &config)
std::ostream &	hal::SMT::operator<< (std::ostream &out, const Constraint &constraint)
std::ostream &	hal::SMT::operator<< (std::ostream &out, const Model &model)
std::ostream &	hal::SMT::operator<< (std::ostream &out, const SolverResult &result)

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