LFSCLem Class Reference

#include <LFSCBoolProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLem:

List of all members.

Public Member Functions

• virtual LFSCLem * AsLFSCLem ()
• void print_pf (std::ostream &s, int ind=0)
• void print_struct (std::ostream &s, int ind=0)
• bool IsTrivial ()
• LFSCProof * clone ()
• int checkBoolRes (std::vector< int > &clause)

Static Public Member Functions

• static LFSCProof * Make (int v)

Private Member Functions

• LFSCLem (int v)
• virtual ~LFSCLem ()
• long int get_length ()

Private Attributes

• int d_var

---

Detailed Description

Definition at line 38 of file LFSCBoolProof.h.

---

Constructor & Destructor Documentation

LFSCLem::LFSCLem

(

int

v

)

[inline, private]

Definition at line 42 of file LFSCBoolProof.h.

Referenced by clone(), and Make().

virtual LFSCLem::~LFSCLem

(

)

[inline, private, virtual]

Definition at line 44 of file LFSCBoolProof.h.

---

Member Function Documentation

long int LFSCLem::get_length

(

)

[inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 45 of file LFSCBoolProof.h.

virtual LFSCLem* LFSCLem::AsLFSCLem

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 47 of file LFSCBoolProof.h.

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

Implements LFSCProof.

Definition at line 48 of file LFSCBoolProof.h.

References CVC3::abs(), and d_var.

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

Reimplemented from LFSCProof.

Definition at line 49 of file LFSCBoolProof.h.

References d_var.

static LFSCProof* LFSCLem::Make

(

int

v

)

[inline, static]

Definition at line 50 of file LFSCBoolProof.h.

References LFSCLem().

Referenced by LFSCConvert::cvc3_to_lfsc().

bool LFSCLem::IsTrivial

(

)

[inline]

Definition at line 51 of file LFSCBoolProof.h.

LFSCProof* LFSCLem::clone

(

)

[inline, virtual]

Implements LFSCProof.

Definition at line 52 of file LFSCBoolProof.h.

References d_var, and LFSCLem().

int LFSCLem::checkBoolRes

(

std::vector< int > &

clause

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 53 of file LFSCBoolProof.h.

References d_var.

---

Member Data Documentation

int LFSCLem::d_var [private]

Definition at line 41 of file LFSCBoolProof.h.

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

---

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

• LFSCBoolProof.h