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:

• /home/runner/work/cbmc/cbmc/src/cprover/state_encoding_targets.h
• /home/runner/work/cbmc/cbmc/src/goto-instrument/horn_encoding.cpp