SimplePath Class Reference

Simple representation of the path within a proof tree. More...

#include <SimplePath.hpp>

Collaboration diagram for SimplePath:

Public Member Functions
	SimplePath ()
	You should () usually never need a more compilcated constructor.
	SimplePath (uint32_t)
	Use this constructor if you know how many predicates there are.
uint32_t	length () const
	Straightforward get method.
void	clear ()
	evert to the empty state without changing num_preds.
void	set_num_preds (size_t num_predicates)
	Set method for num_predicates.
void	push (const Literal &)
	Add a new Literal to the Path.
Literal	back () const
	Get the last Literal in the Path. Non-destructive.
void	pop ()
	Remove the last item from the Path.
bool	test_for_regularity (Clause &) const
	Regularity test.
void	find_limited_reductions (Unifier &, vector< InferenceItem > &, Clause &)
	Given a Clause, find all possible reductions given the current Path, but only for the first Literal in the Clause.
void	find_all_reductions (Unifier &, vector< InferenceItem > &, Clause &)
	Given a Clause, find all possible reductions given the current Path.
void	show_path_only (ostream &)
	Show just the path.
string	to_string (bool=false) const
	Convert the path to a string.
string	make_LaTeX (bool=false) const
	Convert the Path only to a LaTeX representation.
vector< Literal >::const_iterator	cbegin () const
	Iterators just traverse the path vector.
vector< Literal >::const_iterator	cend () const
vector< Literal >::iterator	begin ()
vector< Literal >::iterator	end ()

Private Member Functions
void	find_reductions (Unifier &, vector< InferenceItem > &, const Literal &, LitNum)
	Find the reductions that you can perform for a specified Literal.

Private Attributes
vector< Literal >	path
	Simple representation of a path as a vector of Literals.
uint32_t	num_preds
uint32_t	len

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

Detailed Description

Simple representation of the path within a proof tree.

While the Path class (not part of the source distribution) keeps a separate vector of literals for each possible predicate/negation combination so it's fast to get the potential literals for reductions, this does not. The reason is that this one needs to be copied to support full backtracking, and I haven't yet looked at optimising to see what the trade-off is between finding reductions fast, and making copies of the path_index.

This class is also a natural location for any methods used to find reductions, and a natural location for the test_for_regularity method.

Definition at line 55 of file SimplePath.hpp.

Constructor & Destructor Documentation

SimplePath() [1/2]

SimplePath::SimplePath ( )

inline

You should () usually never need a more compilcated constructor.

Definition at line 82 of file SimplePath.hpp.

: path(), num_preds(0), len(0) {}

SimplePath() [2/2]

SimplePath::SimplePath

(

uint32_t

num_predicates

)

Use this constructor if you know how many predicates there are.

Parameters

num_predicates

Number of predicates.

Definition at line 28 of file SimplePath.cpp.

: path()
, num_preds(num_predicates)
, len(0)
{}

Member Function Documentation

back()

Literal SimplePath::back

(

)

const

Get the last Literal in the Path. Non-destructive.

Definition at line 44 of file SimplePath.cpp.

                               {
  if (len > 0)
    return path.back();
  else {
    cerr << "Stop it - the path is empty!" << endl;
    Literal result;
    return result;
  }
}

begin()

vector< Literal >::iterator SimplePath::begin ( )

inline

Definition at line 181 of file SimplePath.hpp.

{ return path.begin(); }

cbegin()

vector< Literal >::const_iterator SimplePath::cbegin ( ) const

inline

Iterators just traverse the path vector.

Definition at line 179 of file SimplePath.hpp.

{ return path.cbegin(); }

cend()

vector< Literal >::const_iterator SimplePath::cend ( ) const

inline

Definition at line 180 of file SimplePath.hpp.

{ return path.cend(); }

clear()

void SimplePath::clear

(

)

evert to the empty state without changing num_preds.

Definition at line 34 of file SimplePath.cpp.

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

end()

vector< Literal >::iterator SimplePath::end ( )

inline

Definition at line 182 of file SimplePath.hpp.

{ return path.end(); }

find_all_reductions()

void SimplePath::find_all_reductions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c )

Given a Clause, find all possible reductions given the current Path.

See also the documentation for find_reductions.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	A Clause that you want the reductions for.

Definition at line 115 of file SimplePath.cpp.

                                    {
  // Don't waste your time if the path is empty.
  if (len == 0)
    return;
  if (c.size() == 0) {
    cerr << "You shouldn't be looking for reductions with an empty clause" << endl;
    return;
  }
  for (size_t index = 0; index < c.size(); index++) 
    find_reductions(u, result, c[index], index);
}

find_limited_reductions()

void SimplePath::find_limited_reductions	(	Unifier &	u,
		vector< InferenceItem > &	result,
		Clause &	c )

Given a Clause, find all possible reductions given the current Path, but only for the first Literal in the Clause.

See also the documentation for find_reductions.

Parameters

u	A reference to a Unifier function object.
result	A reference to a vector of InferenceItems. Start with this empty.
c	A Clause that you want the reductions for.

Definition at line 102 of file SimplePath.cpp.

                                    {
  // Don't waste your time if the path is empty.
  if (len == 0)
    return;
  if (c.size() == 0) {
    cerr << "You shouldn't be looking for reductions with an empty clause" << endl;
    return;
  }
  find_reductions(u, result, c[0], 0);
}

find_reductions()

void SimplePath::find_reductions ( Unifier & u, vector< InferenceItem > & result, const Literal & lit, LitNum index )

private

Find the reductions that you can perform for a specified Literal.

This process simply requires you to find the complementary Literals in the SimplePath that unify with the one specified.

Parameters

u	A Unifier function object.
result	A reference to a vector of InferenceItems.
lit	A Literal that you want the reductions for.
index	The index of lit. In this instance that means the index (position) in the Clause it comes from.

Definition at line 77 of file SimplePath.cpp.

                                         {
  Literal neg_lit(lit);
  neg_lit.invert();
  size_t path_i = 0;
  for (const Literal& lit2 : path) {
    if (!neg_lit.is_compatible_with(&lit2)) {
      path_i++;
      continue;
    }
    UnificationOutcome outcome = u(neg_lit, lit2);
    if (outcome == UnificationOutcome::Succeed) {
      result.push_back(
        InferenceItem(InferenceItemType::Reduction,
            lit, index, 0, 0,
            u.get_substitution(),
            path_i));
      u.backtrack();
    }
    path_i++;
  }
}

length()

uint32_t SimplePath::length ( ) const

inline

Straightforward get method.

Definition at line 93 of file SimplePath.hpp.

{ return len; }

make_LaTeX()

string SimplePath::make_LaTeX

(

bool

subbed = false

)

const

Convert the Path only to a LaTeX representation.

Parameters

subbed

Implement substitutions if true.

Definition at line 148 of file SimplePath.cpp.

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

pop()

void SimplePath::pop

(

)

Remove the last item from the Path.

Definition at line 54 of file SimplePath.cpp.

                     {
  if (len > 0) {
    path.pop_back();
    len--;
  }
  else {
    cerr << "Stop it - the path is empty!" << endl;
  }
}

push()

void SimplePath::push

(

const Literal &

lit

)

Add a new Literal to the Path.

Parameters

lit	Reference to Literal to add.

Definition at line 39 of file SimplePath.cpp.

                                        {
    path.push_back(lit);
    len++;
}

set_num_preds()

void SimplePath::set_num_preds ( size_t num_predicates )

inline

Set method for num_predicates.

Definition at line 101 of file SimplePath.hpp.

{ num_preds = num_predicates; }

show_path_only()

void SimplePath::show_path_only

(

ostream &

out

)

Show just the path.

Use this if you don't need to see the index and other information.

This method is slightly out of place here as it's mainly for compatability with the Path class, that is not currently part of the distribution, You can probably safely ignore it.

Parameters

out	Reference to an ostream.

Definition at line 129 of file SimplePath.cpp.

                                            {
  out << "Path: ";
  for (auto l : path)
    out << l << " ";
  out << endl;
}

test_for_regularity()

bool SimplePath::test_for_regularity

(

Clause &

c

)

const

Regularity test.

Taking substitutions into account, test whether any literal in the clause appears in the path.

Parameters

c	Reference to Clause to use.

Definition at line 64 of file SimplePath.cpp.

                                                    {
  for (const Literal& lit : path) {
    for (size_t i = 0; i < c.size(); i++)
      if (lit.subbed_equal(&(c[i])))
        return false;
  }
  return true;
}

to_string()

string SimplePath::to_string

(

bool

subbed = false

)

const

Convert the path to a string.

Parameters

subbed

Implement substitution if true.

Definition at line 136 of file SimplePath.cpp.

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

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const SimplePath & p )

friend

Definition at line 159 of file SimplePath.cpp.

                                                       {
    out << "Path:" << endl;
    out << "-----" << endl;
    out << p.to_string();
    return out;
}

Member Data Documentation

len

uint32_t SimplePath::len

private

Definition at line 62 of file SimplePath.hpp.

num_preds

uint32_t SimplePath::num_preds

private

Definition at line 61 of file SimplePath.hpp.

path

vector<Literal> SimplePath::path

private

Simple representation of a path as a vector of Literals.

Definition at line 60 of file SimplePath.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/v0.5.0/source/SimplePath.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/v0.5.0/source/SimplePath.cpp