cprover
graphml_witnesst Class Reference

#include <graphml_witness.h>

+ Collaboration diagram for graphml_witnesst:

Public Member Functions

 graphml_witnesst (const namespacet &_ns)
 
void operator() (const goto_tracet &goto_trace)
 counterexample witness More...
 
void operator() (const symex_target_equationt &equation)
 proof witness More...
 
const graphmltgraph ()
 

Protected Member Functions

void remove_l0_l1 (exprt &expr)
 
std::string convert_assign_rec (const irep_idt &identifier, const code_assignt &assign)
 

Protected Attributes

const namespacetns
 
graphmlt graphml
 

Detailed Description

Definition at line 21 of file graphml_witness.h.

Constructor & Destructor Documentation

◆ graphml_witnesst()

graphml_witnesst::graphml_witnesst ( const namespacet _ns)
inlineexplicit

Definition at line 24 of file graphml_witness.h.

Member Function Documentation

◆ convert_assign_rec()

std::string graphml_witnesst::convert_assign_rec ( const irep_idt identifier,
const code_assignt assign 
)
protected

Definition at line 51 of file graphml_witness.cpp.

◆ graph()

const graphmlt& graphml_witnesst::graph ( )
inline

Definition at line 32 of file graphml_witness.h.

◆ operator()() [1/2]

void graphml_witnesst::operator() ( const goto_tracet goto_trace)

counterexample witness

Definition at line 179 of file graphml_witness.cpp.

◆ operator()() [2/2]

void graphml_witnesst::operator() ( const symex_target_equationt equation)

proof witness

Definition at line 356 of file graphml_witness.cpp.

◆ remove_l0_l1()

void graphml_witnesst::remove_l0_l1 ( exprt expr)
protected

Definition at line 25 of file graphml_witness.cpp.

Member Data Documentation

◆ graphml

graphmlt graphml_witnesst::graphml
protected

Definition at line 39 of file graphml_witness.h.

◆ ns

const namespacet& graphml_witnesst::ns
protected

Definition at line 38 of file graphml_witness.h.


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