Lemmata Class Reference

Representation of the lemma list. More...

#include <Lemmata.hpp>

Collaboration diagram for Lemmata:

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

Private Attributes
vector< Literal >	ls
	Lemmata list as appearing in the connection calculus.
size_t	len

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.

Definition at line 49 of file Lemmata.hpp.

Constructor & Destructor Documentation

Lemmata()

Lemmata::Lemmata ( )

inline

You should not need any more complicated constructor.

Definition at line 60 of file Lemmata.hpp.

: ls(), len(0) {}

Member Function Documentation

clear()

void Lemmata::clear ( )

inline

Self-explanatory.

Definition at line 70 of file Lemmata.hpp.

{ ls.clear(); len = 0; }

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

Definition at line 56 of file Lemmata.cpp.

                                                                    {
  if (len == 0)
    return;
  if (c.size() == 0) {
    cerr << "You shouldn't be looking for lemmata with an empty clause" << endl;
    return;
  }
  size_t i = 0;
  for (const Literal& lit1 : c) {
    size_t lemmata_index = 0;
    for (Literal& lit2 : ls) {
      if (lit1.subbed_equal(&lit2)) {
        inf.push_back(InferenceItem(InferenceItemType::Lemma, 
          lit1, 
          i, 
          lemmata_index));
        // If you've found a way of applying the rule them it 
        // doesn't make any sense to continue.
        break;
      }
      lemmata_index++;
    }
    i++;
  }
}

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

Definition at line 33 of file Lemmata.cpp.

                                                                        {
  if (len == 0)
    return;
  if (c.size() == 0) {
    cerr << "You shouldn't be looking for lemmata with an empty clause" << endl;
    return;
  }
  size_t lemmata_index = 0;
  const Literal& lit1 = c[0];
  for (Literal& lit2 : ls) {
    if (lit1.subbed_equal(&lit2)) {
      inf.push_back(InferenceItem(InferenceItemType::Lemma, 
        lit1, 
        0, 
        lemmata_index));
      // If you've found a way of applying the rule them it 
      // doesn't make any sense to continue.
      return;
    }
    lemmata_index++;
  }
}

make_LaTeX()

string Lemmata::make_LaTeX

(

bool

subbed = false

)

const

Convert to a LaTeX representation.

Parameters

subbed

Implement substitutions if true.

Definition at line 94 of file Lemmata.cpp.

                                            {
  commas::comma com(ls.size());
  string s ("\\textcolor{cyan}{[ }");
  for (const Literal& l : ls) {
        s += l.make_LaTeX(subbed);
        s += com();
  }
  s += "\\textcolor{cyan}{]}";
  return s;
}

push_back()

void Lemmata::push_back

(

const Literal &

l

)

Self-explanatory.

Parameters

l	Reference to Literal to add

Definition at line 28 of file Lemmata.cpp.

                                        {
  ls.push_back(l);
  len++;
}

to_string()

string Lemmata::to_string

(

bool

subbed = false

)

const

Convert to a string.

Parameters

subbed

Implement substitutions if true.

Definition at line 82 of file Lemmata.cpp.

                                           {
  commas::comma com(ls.size());
  string result;
  result += "[ ";
  for (const Literal& l : ls) {
        result += l.to_string(subbed);
        result += com();
  }
  result += " ]";
  return result;
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const Lemmata & l )

friend

Definition at line 105 of file Lemmata.cpp.

                                                    {
  out << "Lemmata:" << endl;
  out << "--------" << endl;
  out << l.to_string();
  return out;
}

Member Data Documentation

len

size_t Lemmata::len

private

Definition at line 55 of file Lemmata.hpp.

ls

vector<Literal> Lemmata::ls

private

Lemmata list as appearing in the connection calculus.

Definition at line 54 of file Lemmata.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/Lemmata.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/Lemmata.cpp