CBMC
smt2_encoding_targett Class Reference
+ Inheritance diagram for smt2_encoding_targett:
+ Collaboration diagram for smt2_encoding_targett:

Public Member Functions

 smt2_encoding_targett (const namespacet &ns, std::ostream &_out)
 
 ~smt2_encoding_targett ()
 
void set_to_true (source_locationt, exprt expr) override
 
void annotation (const std::string &text) override
 
- Public Member Functions inherited from encoding_targett
void set_to_true (exprt expr)
 
void set_source_location (source_locationt __source_location)
 
virtual ~encoding_targett ()=default
 

Protected Attributes

std::ostream & out
 
smt2_convt smt2_conv
 
- Protected Attributes inherited from encoding_targett
source_locationt source_location = source_locationt::nil()
 

Detailed Description

Definition at line 271 of file horn_encoding.cpp.

Constructor & Destructor Documentation

◆ smt2_encoding_targett()

smt2_encoding_targett::smt2_encoding_targett ( const namespacet ns,
std::ostream &  _out 
)
inline

Definition at line 274 of file horn_encoding.cpp.

◆ ~smt2_encoding_targett()

smt2_encoding_targett::~smt2_encoding_targett ( )
inline

Definition at line 282 of file horn_encoding.cpp.

Member Function Documentation

◆ annotation()

void smt2_encoding_targett::annotation ( const std::string &  text)
inlineoverridevirtual

Reimplemented from encoding_targett.

Definition at line 293 of file horn_encoding.cpp.

◆ set_to_true()

void smt2_encoding_targett::set_to_true ( source_locationt  ,
exprt  expr 
)
inlineoverridevirtual

Implements encoding_targett.

Definition at line 288 of file horn_encoding.cpp.

Member Data Documentation

◆ out

std::ostream& smt2_encoding_targett::out
protected

Definition at line 302 of file horn_encoding.cpp.

◆ smt2_conv

smt2_convt smt2_encoding_targett::smt2_conv
protected

Definition at line 303 of file horn_encoding.cpp.


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