CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
smt2_encoding_targett Class Reference

#include <state_encoding_targets.h>

+ 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
 
 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
 
void set_to_true (exprt expr)
 
void set_source_location (source_locationt __source_location)
 
virtual ~encoding_targett ()=default
 

Protected Member Functions

void add_converters ()
 

Protected Attributes

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

Detailed Description

Definition at line 88 of file state_encoding_targets.h.

Constructor & Destructor Documentation

◆ smt2_encoding_targett() [1/2]

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

Definition at line 91 of file state_encoding_targets.h.

◆ ~smt2_encoding_targett() [1/2]

smt2_encoding_targett::~smt2_encoding_targett ( )
inline

Definition at line 96 of file state_encoding_targets.h.

◆ smt2_encoding_targett() [2/2]

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() [2/2]

smt2_encoding_targett::~smt2_encoding_targett ( )
inline

Definition at line 282 of file horn_encoding.cpp.

Member Function Documentation

◆ add_converters()

void smt2_encoding_targett::add_converters ( )
protected

◆ annotation() [1/2]

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

Reimplemented from encoding_targett.

Definition at line 107 of file state_encoding_targets.h.

◆ annotation() [2/2]

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() [1/2]

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

Implements encoding_targett.

Definition at line 102 of file state_encoding_targets.h.

◆ set_to_true() [2/2]

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 116 of file state_encoding_targets.h.

◆ smt2_conv [1/2]

state_encoding_smt2_convt smt2_encoding_targett::smt2_conv
protected

Definition at line 117 of file state_encoding_targets.h.

◆ smt2_conv [2/2]

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 files: