cprover
graphml_witnesst Class Reference

#include <graphml_witness.h>

Collaboration diagram for graphml_witnesst:
[legend]

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()

◆ graph()

const graphmlt& graphml_witnesst::graph ( )
inline

Definition at line 32 of file graphml_witness.h.

References graphml.

Referenced by bmct::output_graphml().

◆ operator()() [1/2]

◆ operator()() [2/2]

◆ remove_l0_l1()

void graphml_witnesst::remove_l0_l1 ( exprt expr)
protected

Member Data Documentation

◆ graphml

graphmlt graphml_witnesst::graphml
protected

Definition at line 39 of file graphml_witness.h.

Referenced by graph(), and operator()().

◆ ns

const namespacet& graphml_witnesst::ns
protected

Definition at line 38 of file graphml_witness.h.

Referenced by convert_assign_rec(), and operator()().


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