hal::SMT::Model Struct Reference

#include <types.h>

Collaboration diagram for hal::SMT::Model:

Public Member Functions
	Model (const std::map< std::string, std::tuple< u64, u16 >> &model={})
bool	operator== (const Model &other) const
bool	operator!= (const Model &other) const
Result< BooleanFunction >	evaluate (const BooleanFunction &bf) const

Static Public Member Functions
static Result< Model >	parse (const std::string &model_str, const SolverType &solver)

Public Attributes
std::map< std::string, std::tuple< u64, u16 > >	model
	maps variable identifiers to a (1) value and (2) its bit-size. More...

Friends
std::ostream &	operator<< (std::ostream &out, const Model &model)

Detailed Description

Represents a list of assignments for variable nodes that yield a satisfiable assignment for a given list of constraints.

Definition at line 226 of file types.h.

Constructor & Destructor Documentation

Model()

hal::SMT::Model::Model

(

const std::map< std::string, std::tuple< u64, u16 >> &

model = {}

)

Constructs a new model from a map of variable names to value and bit-size.

Parameters

[in]

model

- A map from variable name to value and bit-size.

Definition at line 196 of file types.cpp.

Referenced by parse().

Member Function Documentation

evaluate()

Result< BooleanFunction > hal::SMT::Model::evaluate

(

const BooleanFunction &

bf

)

const

Evaluates the given Boolean function by replacing all variables contained in the model with their corresponding value and simplifying the result.

Parameters

[in]

bf

- The Boolean function to evaluate.

Returns

The evaluated function on success, an error otherwise.

Definition at line 261 of file types.cpp.

References hal::BooleanFunction::build(), hal::BooleanFunction::Const(), ERR_APPEND, hal::BooleanFunction::get_nodes(), model, and OK.

operator!=()

bool hal::SMT::Model::operator!=

(

const Model &

other

)

const

Checks whether two SMT models are unequal.

Parameters

[in]

other

- The model to compare again.

Returns

True if both models are unequal, false otherwise.

Definition at line 205 of file types.cpp.

operator==()

bool hal::SMT::Model::operator==

(

const Model &

other

)

const

Checks whether two SMT models are equal.

Parameters

[in]

other

- The model to compare again.

Returns

true if both models are equal, false otherwise.

Definition at line 200 of file types.cpp.

References model.

parse()

Result< Model > hal::SMT::Model::parse ( const std::string &  model_str, const SolverType &  solver  )

static

Parses an SMT-Lib model from a string output by a solver of the given type.

Parameters

[in]	model_str	- The SMT-Lib model string.
[in]	solver	- The solver that computed the model.

Returns

The model on success, an error otherwise.

Definition at line 220 of file types.cpp.

References hal::SMT::Bitwuzla, hal::SMT::Boolector, hal::SMT::ModelParser::BOOLECTOR_MODEL_GRAMMAR, ERR, model, Model(), OK, hal::SMT::ModelParser::parser_context, type, hal::SMT::Z3, and hal::SMT::ModelParser::Z3_MODEL_GRAMMAR.

Referenced by hal::smt_init().

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  out, const Model &  model  )

friend

Passes a human-readable description of the SMT model to the output stream.

Parameters

[in]	out	- The output stream to write to.
[in]	model	- The SMT model.

Returns

A reference to the output stream.

Definition at line 210 of file types.cpp.

Member Data Documentation

model

std::map<std::string, std::tuple<u64, u16> > hal::SMT::Model::model

maps variable identifiers to a (1) value and (2) its bit-size.

Definition at line 233 of file types.h.

Referenced by evaluate(), operator==(), parse(), and hal::smt_init().

---

The documentation for this struct was generated from the following files:

• /home/runner/work/hal/hal/include/hal_core/netlist/boolean_function/types.h
• /home/runner/work/hal/hal/src/netlist/boolean_function/types.cpp