CBMC
ai_domain_factory_location_constructort< domainT > Class Template Reference

#include <ai_domain.h>

+ Inheritance diagram for ai_domain_factory_location_constructort< domainT >:
+ Collaboration diagram for ai_domain_factory_location_constructort< domainT >:

Public Types

typedef ai_domain_factory_baset::statet statet
 
typedef ai_domain_factory_baset::locationt locationt
 
typedef ai_domain_factory_baset::trace_ptrt trace_ptrt
 
- Public Types inherited from ai_domain_factoryt< domainT >
typedef ai_domain_factory_baset::statet statet
 
typedef ai_domain_factory_baset::locationt locationt
 
typedef ai_domain_factory_baset::trace_ptrt trace_ptrt
 
- Public Types inherited from ai_domain_factory_baset
typedef ai_domain_baset statet
 
typedef ai_domain_baset::locationt locationt
 
typedef ai_domain_baset::trace_ptrt trace_ptrt
 

Public Member Functions

std::unique_ptr< statetmake (locationt l) const override
 
- Public Member Functions inherited from ai_domain_factoryt< domainT >
std::unique_ptr< statetcopy (const statet &s) const override
 
bool merge (statet &dest, const statet &src, trace_ptrt from, trace_ptrt to) const override
 
- Public Member Functions inherited from ai_domain_factory_baset
virtual ~ai_domain_factory_baset ()
 

Detailed Description

template<typename domainT>
class ai_domain_factory_location_constructort< domainT >

Definition at line 238 of file ai_domain.h.

Member Typedef Documentation

◆ locationt

Definition at line 243 of file ai_domain.h.

◆ statet

template<typename domainT >
typedef ai_domain_factory_baset::statet ai_domain_factory_location_constructort< domainT >::statet

Definition at line 242 of file ai_domain.h.

◆ trace_ptrt

Definition at line 244 of file ai_domain.h.

Member Function Documentation

◆ make()

template<typename domainT >
std::unique_ptr<statet> ai_domain_factory_location_constructort< domainT >::make ( locationt  l) const
inlineoverridevirtual

Implements ai_domain_factory_baset.

Definition at line 246 of file ai_domain.h.


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