LFSCLraAxiom Class Reference

#include <LFSCLraProof.h>

Inherits LFSCProof.

Collaboration diagram for LFSCLraAxiom:

List of all members.

Public Member Functions

• virtual LFSCLraAxiom * AsLFSCLraAxiom ()
• void print_pf (std::ostream &s, int ind=0)
• bool isTrivial ()
• LFSCProof * clone ()
• int checkOp ()

Static Public Member Functions

• static LFSCProof * MakeEq ()
• static LFSCProof * Make (Rational r, int op)

Private Member Functions

• LFSCLraAxiom (int op)
• LFSCLraAxiom (int op, Rational r)
• virtual ~LFSCLraAxiom ()
• long int get_length ()

Private Attributes

• int d_op
• Rational d_r

Static Private Attributes

• static RefPtr< LFSCProof > eq

---

Detailed Description

Definition at line 35 of file LFSCLraProof.h.

---

Constructor & Destructor Documentation

LFSCLraAxiom::LFSCLraAxiom

(

int

op

)

[inline, private]

Definition at line 40 of file LFSCLraProof.h.

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

LFSCLraAxiom::LFSCLraAxiom	(	int	op,
		Rational	r
	)		[inline, private]

Definition at line 41 of file LFSCLraProof.h.

virtual LFSCLraAxiom::~LFSCLraAxiom

(

)

[inline, private, virtual]

Definition at line 44 of file LFSCLraProof.h.

---

Member Function Documentation

long int LFSCLraAxiom::get_length

(

)

[inline, private, virtual]

Reimplemented from LFSCProof.

Definition at line 45 of file LFSCLraProof.h.

virtual LFSCLraAxiom* LFSCLraAxiom::AsLFSCLraAxiom

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 47 of file LFSCLraProof.h.

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

Implements LFSCProof.

Definition at line 44 of file LFSCLraProof.cpp.

References d_op, d_r, EQ, kind_to_str(), and print_rational().

bool LFSCLraAxiom::isTrivial

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 49 of file LFSCLraProof.h.

References d_op, and EQ.

LFSCProof * LFSCLraAxiom::MakeEq

(

)

[static]

Definition at line 37 of file LFSCLraProof.cpp.

References EQ, eq, RefPtr< T >::get(), and LFSCLraAxiom().

Referenced by LFSCConvert::cvc3_to_lfsc().

static LFSCProof* LFSCLraAxiom::Make	(	Rational	r,
		int	op
	)		[inline, static]

Definition at line 51 of file LFSCLraProof.h.

References LFSCLraAxiom().

LFSCProof* LFSCLraAxiom::clone

(

)

[inline, virtual]

Implements LFSCProof.

Definition at line 52 of file LFSCLraProof.h.

References d_op, d_r, and LFSCLraAxiom().

int LFSCLraAxiom::checkOp

(

)

[inline, virtual]

Reimplemented from LFSCProof.

Definition at line 53 of file LFSCLraProof.h.

References d_op.

---

Member Data Documentation

RefPtr< LFSCProof > LFSCLraAxiom::eq [static, private]

Definition at line 37 of file LFSCLraProof.h.

Referenced by MakeEq().

int LFSCLraAxiom::d_op [private]

Definition at line 38 of file LFSCLraProof.h.

Referenced by checkOp(), clone(), isTrivial(), and print_pf().

Rational LFSCLraAxiom::d_r [private]

Definition at line 39 of file LFSCLraProof.h.

Referenced by clone(), and print_pf().

---

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

• LFSCLraProof.h
• LFSCLraProof.cpp