CVC3: LFSCProofGeneric Class Reference

CVC3

#include <LFSCUtilProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCProofGeneric:

Collaboration graph

List of all members.

Public Member Functions

virtual LFSCProofGeneric * AsLFSCProofGeneric ()
void print_pf (std::ostream &s, int ind=0)
LFSCProof * clone ()
int getNumChildren ()
LFSCProof * getChild (int n)

Static Public Member Functions

static LFSCProof * Make (vector< RefPtr< LFSCProof > > &d_pfs, std::vector< string > &d_strs, bool db_str=false)
static LFSCProof * Make (string str_pre, LFSCProof *sub_pf, string str_post, bool db_str=false)
static LFSCProof * Make (string str_pre, LFSCProof *sub_pf1, LFSCProof *sub_pf2, string str_post, bool db_str=false)
static LFSCProof * MakeStr (const char *c, bool db_str=false)
static LFSCProof * MakeUnk ()

Private Member Functions

LFSCProofGeneric (vector< RefPtr< LFSCProof > > &d_pfs, vector< string > &d_strs, bool db_str=false)
virtual ~LFSCProofGeneric ()
long int get_length ()

Private Attributes

vector< RefPtr< LFSCProof > > d_pf
vector< string > d_str
bool debug_str

Detailed Description

Definition at line 61 of file LFSCUtilProof.h.

Constructor & Destructor Documentation

LFSCProofGeneric::LFSCProofGeneric	(	vector< RefPtr< LFSCProof > > &	d_pfs,
		vector< string > &	d_strs,
		bool	db_str = `false`
	)		`[inline, private]`

Definition at line 67 of file LFSCUtilProof.h.

References d_pf, d_str, and debug_str.

Referenced by clone(), Make(), and MakeStr().

virtual LFSCProofGeneric::~LFSCProofGeneric ( ) [inline, private, virtual]

Definition at line 74 of file LFSCUtilProof.h.

Member Function Documentation

long int LFSCProofGeneric::get_length ( ) [private, virtual]

Reimplemented from LFSCProof.

Definition at line 70 of file LFSCUtilProof.cpp.

References d_pf, d_str, debug_str, and LFSCProof::get_string_length().

virtual LFSCProofGeneric* LFSCProofGeneric::AsLFSCProofGeneric ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 77 of file LFSCUtilProof.h.

void LFSCProofGeneric::print_pf	(	std::ostream &	s,
		int	ind = `0`
	)		`[virtual]`

Implements LFSCProof.

Definition at line 81 of file LFSCUtilProof.cpp.

References d_pf, and d_str.

static LFSCProof* LFSCProofGeneric::Make	(	vector< RefPtr< LFSCProof > > &	d_pfs,
		std::vector< string > &	d_strs,
		bool	db_str = `false`
	)		`[inline, static]`

Definition at line 80 of file LFSCUtilProof.h.

References LFSCProofGeneric().

Referenced by LFSCConvert::convert(), LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCProof::Make_and_elim(), LFSCProof::Make_CNF(), LFSCProof::Make_mimic(), LFSCProof::Make_not_not_elim(), and TReturn::normalize_tr().

LFSCProof * LFSCProofGeneric::Make	(	string	str_pre,
		LFSCProof *	sub_pf,
		string	str_post,
		bool	db_str = `false`
	)		`[static]`

Definition at line 90 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

LFSCProof * LFSCProofGeneric::Make	(	string	str_pre,
		LFSCProof *	sub_pf1,
		LFSCProof *	sub_pf2,
		string	str_post,
		bool	db_str = `false`
	)		`[static]`

Definition at line 100 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

LFSCProof * LFSCProofGeneric::MakeStr	(	const char *	c,
		bool	db_str = `false`
	)		`[static]`

Definition at line 113 of file LFSCUtilProof.cpp.

References LFSCProofGeneric().

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCProof::Make_CNF(), LFSCConvert::make_trusted(), MakeUnk(), and TReturn::normalize_tr().

static LFSCProof* LFSCProofGeneric::MakeUnk ( ) [inline, static]

Definition at line 88 of file LFSCUtilProof.h.

References MakeStr().

Referenced by LFSCConvert::cvc3_to_lfsc().

LFSCProof* LFSCProofGeneric::clone ( ) [inline, virtual]

Implements LFSCProof.

Definition at line 89 of file LFSCUtilProof.h.

References d_pf, d_str, debug_str, and LFSCProofGeneric().

int LFSCProofGeneric::getNumChildren ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 90 of file LFSCUtilProof.h.

References d_pf.

LFSCProof* LFSCProofGeneric::getChild ( int n ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 91 of file LFSCUtilProof.h.

References d_pf.

Member Data Documentation

vector< RefPtr< LFSCProof > > LFSCProofGeneric::d_pf [private]

Definition at line 63 of file LFSCUtilProof.h.

Referenced by clone(), get_length(), getChild(), getNumChildren(), LFSCProofGeneric(), and print_pf().

vector< string > LFSCProofGeneric::d_str [private]

Definition at line 64 of file LFSCUtilProof.h.

Referenced by clone(), get_length(), LFSCProofGeneric(), and print_pf().

bool LFSCProofGeneric::debug_str [private]

Definition at line 65 of file LFSCUtilProof.h.

Referenced by clone(), get_length(), and LFSCProofGeneric().

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