Lemmata Class Reference

Representation of the lemma list. More...

#include <Lemmata.hpp>

Public Member Functions
	Lemmata ()
	You should not need any more complicated constructor.
void	push_back (const Literal &)
	Self-explanatory.
void	clear ()
	Self-explanatory.
void	find_all_lemmata (vector< InferenceItem > &, Clause &)
	Find all lemmata that are applicable, given a Clause.
void	find_initial_lemmata (vector< InferenceItem > &, Clause &)
	Find all lemmata that are applicable, but only for the initial Literal in a Clause.
string	to_string (bool=false) const
	Convert to a string.
string	make_LaTeX (bool=false) const

Friends
ostream &	operator<< (ostream &, const Lemmata &)

Detailed Description

Representation of the lemma list.

This is mostly straightforward is it is just a vector of Literals.

However it does have two critical methods: find_all_lemmata and find_initial_lemmata. You should probably read the documentation for these.

Member Function Documentation

find_all_lemmata()

void Lemmata::find_all_lemmata	(	vector< InferenceItem > &	inf,
		Clause &	c
	)

Find all lemmata that are applicable, given a Clause.

The connection calculus allows this, but there is a question of how you implement it. I suspect, but am not 100% certain, that leanCop only looks at the first Literal in the Clause, whereas this looks at all Literals in the Clause. For the (suspected) leanCop behavious use find_initial_lemmata.

In Connect++ the parameter params::all_lemmata controls this and is false by default.

Parameters

inf	Reference to a vector of InferenceItem
c	Reference to a Clause

find_initial_lemmata()

void Lemmata::find_initial_lemmata	(	vector< InferenceItem > &	inf,
		Clause &	c
	)

Find all lemmata that are applicable, but only for the initial Literal in a Clause.

See also the documentation for find_all_lemmata.

Parameters

inf	Reference to a vector of InferenceItem
c	Reference to a Clause

make_LaTeX()

string Lemmata::make_LaTeX

(

bool

subbed = false

)

const

Convert to a LaTeX representation.

Parameters

subbed

Implement substitutions if true.

push_back()

void Lemmata::push_back

(

const Literal &

l

)

Self-explanatory.

Parameters

l	Reference to Literal to add

to_string()

string Lemmata::to_string

(

bool

subbed = false

)

const

Convert to a string.

Parameters

subbed

Implement substitutions if true.

---

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

• Lemmata.hpp
• Lemmata.cpp