#include <LFSCBoolProof.h>

Inheritance diagram for LFSCAssume:

Public Member Functions

virtual LFSCAssume * AsLFSCAssume ()
void print_pf (std::ostream &s, int ind=0)
void print_struct (std::ostream &s, int ind=0)
LFSCProof * clone ()
int getNumChildren ()
LFSCProof * getChild (int n)
int checkBoolRes (std::vector< int > &clause)

Static Public Member Functions

static LFSCProof * Make (int v, LFSCProof *pf, bool assm=true, int type=3)

Private Member Functions

LFSCAssume (int v, LFSCProof *pf, bool assm, int type)
virtual ~LFSCAssume ()
long int get_length ()

Private Attributes

Constructor & Destructor Documentation

LFSCAssume::LFSCAssume	(	int	v,
		LFSCProof *	pf,
		bool	assm,
		int	type
	)		`[inline, private]`

Definition at line 96 of file LFSCBoolProof.h.

Referenced by Make(), and clone().

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

Definition at line 97 of file LFSCBoolProof.h.

Member Function Documentation

long int LFSCAssume::get_length ( ) [inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 98 of file LFSCBoolProof.h.

References d_pf.

virtual LFSCAssume* LFSCAssume::AsLFSCAssume ( ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 100 of file LFSCBoolProof.h.

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

Implements LFSCProof.

Definition at line 161 of file LFSCBoolProof.cpp.

References d_assm, d_var, d_type, CVC3::abs(), and d_pf.

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

Reimplemented from LFSCProof.

Definition at line 172 of file LFSCBoolProof.cpp.

References d_assm, d_var, and d_pf.

static LFSCProof* LFSCAssume::Make	(	int	v,
		LFSCProof *	pf,
		bool	assm = `true`,
		int	type = `3`
	)		`[inline, static]`

Definition at line 103 of file LFSCBoolProof.h.

References LFSCAssume().

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

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

Implements LFSCProof.

Definition at line 106 of file LFSCBoolProof.h.

References LFSCAssume(), d_var, d_pf, RefPtr::get(), d_assm, and d_type.

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

Reimplemented from LFSCProof.

Definition at line 107 of file LFSCBoolProof.h.

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

Reimplemented from LFSCProof.

Definition at line 108 of file LFSCBoolProof.h.

References d_pf, and RefPtr::get().

int LFSCAssume::checkBoolRes ( std::vector< int > & clause ) [inline, virtual]

Reimplemented from LFSCProof.

Definition at line 110 of file LFSCBoolProof.h.

References d_type, d_pf, and d_var.

Member Data Documentation

int LFSCAssume::d_var [private]

Definition at line 92 of file LFSCBoolProof.h.

Referenced by print_pf(), print_struct(), clone(), and checkBoolRes().

RefPtr< LFSCProof > LFSCAssume::d_pf [private]

Definition at line 93 of file LFSCBoolProof.h.

Referenced by print_pf(), print_struct(), get_length(), clone(), getChild(), and checkBoolRes().

bool LFSCAssume::d_assm [private]

Definition at line 94 of file LFSCBoolProof.h.

Referenced by print_pf(), print_struct(), and clone().

int LFSCAssume::d_type [private]

Definition at line 95 of file LFSCBoolProof.h.

Referenced by print_pf(), clone(), and checkBoolRes().

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