LFSCAssume Class Reference

#include <LFSCBoolProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCAssume:

List of all members.

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

• int d_var
• RefPtr< LFSCProof > d_pf
• bool d_assm
• int d_type

---

Detailed Description

Definition at line 90 of file LFSCBoolProof.h.

---

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 clone(), and Make().

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 CVC3::abs(), d_assm, d_pf, d_type, and d_var.

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_pf, and d_var.

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_to_tf(), and TReturn::normalize_tr().

LFSCProof* LFSCAssume::clone

(

)

[inline, virtual]

Implements LFSCProof.

Definition at line 106 of file LFSCBoolProof.h.

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

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< T >::get().

int LFSCAssume::checkBoolRes

(

std::vector< int > &

clause

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 110 of file LFSCBoolProof.h.

References d_pf, d_type, and d_var.

---

Member Data Documentation

int LFSCAssume::d_var [private]

Definition at line 92 of file LFSCBoolProof.h.

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

RefPtr< LFSCProof > LFSCAssume::d_pf [private]

Definition at line 93 of file LFSCBoolProof.h.

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

bool LFSCAssume::d_assm [private]

Definition at line 94 of file LFSCBoolProof.h.

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

int LFSCAssume::d_type [private]

Definition at line 95 of file LFSCBoolProof.h.

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

---

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

• LFSCBoolProof.h
• LFSCBoolProof.cpp