hal::SMT::SolverResult Struct Reference

#include <types.h>

Collaboration diagram for hal::SMT::SolverResult:

Public Member Functions
	SolverResult ()
	Default constructor (required for Result<T> initialization) More...
bool	is (const SolverResultType &type) const
bool	is_sat () const
bool	is_unsat () const
bool	is_unknown () const

Static Public Member Functions
static SolverResult	Sat (const std::optional< Model > &model={})
static SolverResult	UnSat ()
static SolverResult	Unknown ()

Public Attributes
SolverResultType	type
	Result type of the SMT query. More...
std::optional< Model >	model
	The (optional) model that is only available if type == SMT::ResultType::Sat and model generation is enabled. More...

Friends
std::ostream &	operator<< (std::ostream &out, const SolverResult &result)

Detailed Description

Represents the result of an SMT query.

Definition at line 296 of file types.h.

Constructor & Destructor Documentation

SolverResult()

hal::SMT::SolverResult::SolverResult ( )

inline

Default constructor (required for Result<T> initialization)

Definition at line 312 of file types.h.

Referenced by Sat(), Unknown(), and UnSat().

Member Function Documentation

is()

bool hal::SMT::SolverResult::is

(

const SolverResultType &

type

)

const

Checks whether the result is of a specific type.

Parameters

[in]

type

- The type to check.

Returns

true in case result matches the given type, false otherwise.

Definition at line 314 of file types.cpp.

References type.

Referenced by is_sat(), is_unknown(), is_unsat(), and hal::smt_init().

is_sat()

bool hal::SMT::SolverResult::is_sat

(

)

const

Checks whether the result is satisfiable.

Returns

true in case result is satisfiable, false otherwise.

Definition at line 319 of file types.cpp.

References is(), and hal::SMT::Sat.

Referenced by hal::smt_init().

is_unknown()

bool hal::SMT::SolverResult::is_unknown

(

)

const

Checks whether the result is unknown.

Returns

true in case result is unknown, false otherwise.

Definition at line 329 of file types.cpp.

References is(), and hal::SMT::Unknown.

Referenced by hal::smt_init().

is_unsat()

bool hal::SMT::SolverResult::is_unsat

(

)

const

Checks whether the result is unsatisfiable.

Returns

true in case result is unsatisfiable, false otherwise.

Definition at line 324 of file types.cpp.

References is(), and hal::SMT::UnSat.

Referenced by hal::smt_init().

Sat()

SolverResult hal::SMT::SolverResult::Sat ( const std::optional< Model > &  model = {} )

static

Creates a satisfiable result with an optional model.

Parameters

[in]

model

- Optional model for satisfiable formula.

Returns

The result.

Definition at line 299 of file types.cpp.

References model, hal::SMT::Sat, and SolverResult().

Referenced by hal::smt_init().

Unknown()

SolverResult hal::SMT::SolverResult::Unknown ( )

static

Creates an unknown result.

Returns

The result.

Definition at line 309 of file types.cpp.

References SolverResult(), and hal::SMT::Unknown.

Referenced by hal::smt_init().

UnSat()

SolverResult hal::SMT::SolverResult::UnSat ( )

static

Creates an unsatisfiable result.

Returns

The result.

Definition at line 304 of file types.cpp.

References SolverResult(), and hal::SMT::UnSat.

Referenced by hal::smt_init().

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  out, const SolverResult &  result  )

friend

Human-readable description of SMT result.

Parameters

[in]	out	- Stream to write to.
[in]	result	- SMT result.

Returns

A reference to output stream.

Definition at line 334 of file types.cpp.

Member Data Documentation

model

std::optional<Model> hal::SMT::SolverResult::model

The (optional) model that is only available if type == SMT::ResultType::Sat and model generation is enabled.

Definition at line 305 of file types.h.

Referenced by Sat(), and hal::smt_init().

type

SolverResultType hal::SMT::SolverResult::type

Result type of the SMT query.

Definition at line 303 of file types.h.

Referenced by is(), 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