cprover
Classes | Public Types | Public Member Functions | Public Attributes | List of all members
bmc_covert::goalt Struct Reference
Collaboration diagram for bmc_covert::goalt:
[legend]

Classes

struct  instancet
 

Public Types

typedef std::vector< instancet > instancest
 

Public Member Functions

void add_instance (symex_target_equationt::SSA_stepst::iterator step, literalt condition)
 
 goalt (const std::string &_description, const source_locationt &_source_location)
 
 goalt ()
 
exprt as_expr () const
 

Public Attributes

instancest instances
 
std::string description
 
source_locationt source_location
 
bool satisfied
 

Detailed Description

Definition at line 48 of file bmc_cover.cpp.

Member Typedef Documentation

◆ instancest

typedef std::vector<instancet> bmc_covert::goalt::instancest

Definition at line 57 of file bmc_cover.cpp.

Constructor & Destructor Documentation

◆ goalt() [1/2]

bmc_covert::goalt::goalt ( const std::string &  _description,
const source_locationt &  _source_location 
)
inline

Definition at line 75 of file bmc_cover.cpp.

◆ goalt() [2/2]

bmc_covert::goalt::goalt ( )
inline

Definition at line 84 of file bmc_cover.cpp.

Member Function Documentation

◆ add_instance()

void bmc_covert::goalt::add_instance ( symex_target_equationt::SSA_stepst::iterator  step,
literalt  condition 
)
inline

Definition at line 60 of file bmc_cover.cpp.

References instances.

◆ as_expr()

exprt bmc_covert::goalt::as_expr ( ) const
inline

Definition at line 89 of file bmc_cover.cpp.

References disjunction(), and instances.

Member Data Documentation

◆ description

std::string bmc_covert::goalt::description

Definition at line 69 of file bmc_cover.cpp.

Referenced by bmc_covert::operator()(), and bmc_covert::satisfying_assignment().

◆ instances

instancest bmc_covert::goalt::instances

Definition at line 58 of file bmc_cover.cpp.

Referenced by add_instance(), as_expr(), and bmc_covert::satisfying_assignment().

◆ satisfied

bool bmc_covert::goalt::satisfied

Definition at line 73 of file bmc_cover.cpp.

Referenced by bmc_covert::operator()(), and bmc_covert::satisfying_assignment().

◆ source_location

source_locationt bmc_covert::goalt::source_location

Definition at line 70 of file bmc_cover.cpp.

Referenced by bmc_covert::operator()().

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