HAL
Public Member Functions | Public Attributes | Friends | List of all members
hal::SMT::Constraint Struct Referencefinal

#include <types.h>

Collaboration diagram for hal::SMT::Constraint:
Collaboration graph

Public Member Functions

 Constraint (BooleanFunction &&constraint)
 
 Constraint (BooleanFunction &&lhs, BooleanFunction &&rhs)
 
std::string to_string () const
 
bool is_assignment () const
 
Result< const std::pair< BooleanFunction, BooleanFunction > * > get_assignment () const
 
Result< const BooleanFunction * > get_function () const
 

Public Attributes

std::variant< BooleanFunction, std::pair< BooleanFunction, BooleanFunction > > constraint
 A constraint that is either an assignment of two Boolean functions or a single Boolean function, e.g., an equality check or similar. More...
 

Friends

std::ostream & operator<< (std::ostream &out, const Constraint &constraint)
 

Detailed Description

Represents a constraint to the SMT query. A constraint is either an assignment of two Boolean functions or a single Boolean function, e.g., an equality check or similar.

Definition at line 147 of file types.h.

Constructor & Destructor Documentation

◆ Constraint() [1/2]

hal::SMT::Constraint::Constraint ( BooleanFunction &&  constraint)
explicit

Constructs a new constraint from one Boolean function that evaluates to a single bit.

Parameters
[in]constraint- The constraint function.

Definition at line 143 of file types.cpp.

◆ Constraint() [2/2]

hal::SMT::Constraint::Constraint ( BooleanFunction &&  lhs,
BooleanFunction &&  rhs 
)
explicit

Constructs a new equality constraint from two Boolean functions.

Parameters
[in]lhs- The left-hand side of the equality constraint
[in]rhs- The right-hand side of the equality constraint

Definition at line 147 of file types.cpp.

Member Function Documentation

◆ get_assignment()

Result< const std::pair< BooleanFunction, BooleanFunction > * > hal::SMT::Constraint::get_assignment ( ) const

Returns the assignment constraint as a pair of Boolean functions.

Returns
The assignment constraint on success, an error otherwise.

Definition at line 178 of file types.cpp.

References constraint, ERR, is_assignment(), and OK.

Referenced by hal::SMT::SymbolicExecution::evaluate().

◆ get_function()

Result< const BooleanFunction * > hal::SMT::Constraint::get_function ( ) const

Returns the function constraint.

Returns
The function constraint on success, an error otherwise.

Definition at line 187 of file types.cpp.

References constraint, ERR, is_assignment(), and OK.

◆ is_assignment()

bool hal::SMT::Constraint::is_assignment ( ) const

Checks whether the constraint is an assignment constraint.

Returns
true if the constraint is an assignment, false otherwise.

Definition at line 173 of file types.cpp.

References constraint.

Referenced by hal::SMT::SymbolicExecution::evaluate(), get_assignment(), get_function(), and hal::smt_init().

◆ to_string()

std::string hal::SMT::Constraint::to_string ( ) const

Translate the SMT constraint into its string representation.

Returns
A string representing the SMT constraint.

Definition at line 166 of file types.cpp.

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  out,
const Constraint &  constraint 
)
friend

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

Parameters
[in]out- The output stream to write to.
[in]constraint- The SMT constraint.
Returns
A reference to the output stream.

Definition at line 151 of file types.cpp.

Member Data Documentation

◆ constraint

std::variant<BooleanFunction, std::pair<BooleanFunction, BooleanFunction> > hal::SMT::Constraint::constraint

A constraint that is either an assignment of two Boolean functions or a single Boolean function, e.g., an equality check or similar.

Definition at line 154 of file types.h.

Referenced by get_assignment(), get_function(), is_assignment(), and hal::smt_init().

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